mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case coe
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
ω : Ω
a✝ : ι
⊢ u (min (↑(↑a✝).untopA) (τ ω)).untopA ω =
    if ↑a✝ = ⊤ then u (min (↑(Classical.arbitrary ι)) (τ ω)).untopA ω else u (min (↑a✝) (τ ω)).untopA ω

Tactic:
cases τ ω

Goal state after:
case coe.top
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
ω : Ω
a✝ : ι
⊢ u (min ↑(↑a✝).untopA ⊤).untopA ω =
    if ↑a✝ = ⊤ then u (min ↑(Classical.arbitrary ι) ⊤).untopA ω else u (min ↑a✝ ⊤).untopA ω

case coe.coe
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
ω : Ω
a✝¹ a✝ : ι
⊢ u (min ↑(↑a✝¹).untopA ↑a✝).untopA ω =
    if ↑a✝¹ = ⊤ then u (min ↑(Classical.arbitrary ι) ↑a✝).untopA ω else u (min ↑a✝¹ ↑a✝).untopA ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
f : Filtration ι m
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
t : Set β
ht : MeasurableSet t
i : ι
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
this : stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ ↑i} = (stoppedValue u fun ω ↦ min (τ ω) ↑i) ⁻¹' t ∩ {ω | τ ω ≤ ↑i}
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ ↑i})

Tactic:
by
    rw [this]; exact ((h_str_meas i).measurable ht).inter (hτ.measurableSet_le i)

Goal state after:
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ ∫ (x : Ω), (fun ω ↦ rexp (t * (α + X ω))) x ∂μ = ∫ (a : Ω), rexp (t * α) * rexp (t * X a) ∂μ

Tactic:
congr with x

Goal state after:
case e_f
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
x : Ω
⊢ (fun ω ↦ rexp (t * (α + X ω))) x = rexp (t * α) * rexp (t * X x)
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
ι : Type u_3
μ : ι → Measure Ω
hμ : Integrable (fun ω ↦ rexp (t * X ω)) (Measure.sum μ)
⊢ mgf X (Measure.sum μ) t = ∑' (i : ι), mgf X (μ i) t

Tactic:
by
  simp_rw [mgf, integral_sum_measure hμ]

Goal state after:
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

Tactic:
by
  have A : Continuous fun x : ℝ => exp (t * x) := by fun_prop
  have h'X : AEStronglyMeasurable (fun ω => exp (t * X ω)) μ :=
    A.aestronglyMeasurable.comp_aemeasurable hX.aemeasurable
  have h'Y : AEStronglyMeasurable (fun ω => exp (t * Y ω)) μ :=
    A.aestronglyMeasurable.comp_aemeasurable hY.aemeasurable
  exact h_indep.mgf_add h'X h'Y

Goal state after:
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: μ : Measure ℝ
t : ℝ
⊢ ∫ (ω : ℝ), cexp (↑t * I * ↑ω) ∂μ = ∫ (x : ℝ), cexp (↑t * ↑x * I) ∂μ

Tactic:
congr with x

Goal state after:
case e_f
μ : Measure ℝ
t x : ℝ
⊢ cexp (↑t * I * ↑x) = cexp (↑t * ↑x * I)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁴ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : Ω → E
hτ : IsStoppingTime ℱ τ
i : ι
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ μ[f | ⋯.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ ↑i}] μ[f | hτ.measurableSpace]

Tactic:
have : SigmaFinite (μ.trim hτ.measurableSpace_le) :=
    haveI h_le : (hτ.min_const i).measurableSpace ≤ hτ.measurableSpace := by
      rw [IsStoppingTime.measurableSpace_min_const]
      exact inf_le_left
    sigmaFiniteTrim_mono _ h_le
  refine (condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le
    (hτ.min_const i).measurableSpace_le (hτ.measurableSet_le' i) fun t => ?_).symm
  rw [Set.inter_comm _ t, hτ.measurableSet_inter_le_const_iff]

Goal state after:
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    t ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
this : deriv (iteratedDeriv n (mgf X μ)) =ᶠ[𝓝 t] fun t ↦ ∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ
⊢ HasDerivAt (deriv (iteratedDeriv n (mgf X μ))) (∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t

Tactic:
EventuallyEq.hasDerivAt_iff this

Goal state after:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    t ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
this : deriv (iteratedDeriv n (mgf X μ)) =ᶠ[𝓝 t] fun t ↦ ∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ
⊢ HasDerivAt (fun t ↦ ∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ)
    (∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
⊢ AnalyticOnNhd ℝ (iteratedDeriv n (mgf X μ)) (interior (integrableExpSet X μ))

Tactic:
rw [iteratedDeriv_eq_iterate]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
⊢ AnalyticOnNhd ℝ (deriv^[n] (mgf X μ)) (interior (integrableExpSet X μ))
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ∫ (x : ℝ), gaussianPDFReal μ v x = 1

Tactic:
by
  have h := lintegral_gaussianPDFReal_eq_one μ hv
  rw [← ofReal_integral_eq_lintegral_ofReal (integrable_gaussianPDFReal _ _)
    (ae_of_all _ (gaussianPDFReal_nonneg _ _)), ← ENNReal.ofReal_one] at h
  rwa [← ENNReal.ofReal_eq_ofReal_iff (integral_nonneg (gaussianPDFReal_nonneg _ _)) zero_le_one]

Goal state after:
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2.refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
h_le : ∀ (a : Ω), |X a| ^ p * rexp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)
ω : Ω
⊢ ‖||X ω| ^ p| * rexp (v * X ω + x * |X ω|)‖ ≤ ‖(p / (|t| - x)) ^ p * rexp (v * X ω + |t| * |X ω|)‖

Tactic:
· simp only [norm_mul, norm_eq_abs, abs_exp]
    simp_rw [abs_rpow_of_nonneg (abs_nonneg _), abs_abs]
    refine (h_le ω).trans_eq ?_
    congr
    symm
    simp only [abs_eq_self]
    positivity [sub_nonneg_of_le hx.le]

Goal state after:
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
this :
  deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun z ↦
    ∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ
⊢ HasDerivAt (deriv (iteratedDeriv n (complexMGF X μ)))
    (∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1 + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
EventuallyEq.hasDerivAt_iff this

Goal state after:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
this :
  deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun z ↦
    ∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ
⊢ HasDerivAt (fun z ↦ ∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ)
    (∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1 + 1) * cexp (z * ↑(X ω))) x ∂μ) z
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : μ = 0
⊢ Integrable (fun ω ↦ rexp (t * X ω)) μ ↔ Integrable (fun ω ↦ rexp (t * Y ω)) μ'

pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : ¬μ = 0
⊢ Integrable (fun ω ↦ rexp (t * X ω)) μ ↔ Integrable (fun ω ↦ rexp (t * Y ω)) μ'

Tactic:
· simp [hμ, hμμ'.mp hμ]

Goal state after:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : ¬μ = 0
⊢ Integrable (fun ω ↦ rexp (t * X ω)) μ ↔ Integrable (fun ω ↦ rexp (t * Y ω)) μ'
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case neg
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
⊢ Measure.map (fun x ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)

Tactic:
have he' : ∀ x, HasDerivAt e ((fun _ ↦ c⁻¹) x) x := by
    suffices ∀ x, HasDerivAt (fun x => c⁻¹ * x) (c⁻¹ * 1) x by rwa [mul_one] at this
    exact fun _ ↦ HasDerivAt.const_mul _ (hasDerivAt_id _)

Goal state after:
case neg
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
⊢ Measure.map (fun x ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case neg
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal (∫ (x : ℝ) in s', |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v) x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v) x)

Tactic:
congr with x

Goal state after:
case neg.e_f
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
⊢ |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v) x) =
    gaussianPDFReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v) x
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ (↑√(2 * (π * ↑v)))⁻¹ * ∫ (a : ℝ), cexp (-(↑a - ↑μ) ^ 2 / (2 * ↑↑v) + z * ↑a) =
    (↑√(2 * (π * ↑v)))⁻¹ * ∫ (x : ℝ), cexp (-(2 * ↑↑v)⁻¹ * ↑x ^ 2 + (z + ↑μ / ↑↑v) * ↑x + -↑μ ^ 2 / (2 * ↑↑v))

Tactic:
congr with x

Goal state after:
case e_a.e_f
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
x : ℝ
⊢ cexp (-(↑x - ↑μ) ^ 2 / (2 * ↑↑v) + z * ↑x) = cexp (-(2 * ↑↑v)⁻¹ * ↑x ^ 2 + (z + ↑μ / ↑↑v) * ↑x + -↑μ ^ 2 / (2 * ↑↑v))
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case pos
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
⊢ ∫ (x_1 : E),
      ⟪x, c + x_1 - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫ *
        ⟪y, c + x_1 - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫ ∂μ =
    ∫ (z : E), ⟪x, z - ∫ (x : E), id x ∂μ⟫ * ⟪y, z - ∫ (x : E), id x ∂μ⟫ ∂μ

Tactic:
congr with z

Goal state after:
case pos.e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
z : E
⊢ ⟪x, c + z - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫ *
      ⟪y, c + z - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫ =
    ⟪x, z - ∫ (x : E), id x ∂μ⟫ * ⟪y, z - ∫ (x : E), id x ∂μ⟫
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (gaussianReal m₁ v₁)

Tactic:
apply IsFiniteMeasure.toSigmaFinite

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case σg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (gaussianReal m₂ v₂)

Tactic:
apply IsFiniteMeasure.toSigmaFinite

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
⊢ Continuous[ContinuousLinearMap.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (toLpₗ μ p).toFun

Tactic:
refine LinearMap.continuous_of_locally_bounded _ fun s hs ↦ ?_
    rw [image_isVonNBounded_iff]
    simp_rw [isVonNBounded_iff'] at hs
    obtain ⟨r, hxr⟩ := hs
    refine ⟨r * (eLpNorm id p μ).toReal, fun L hLs ↦ ?_⟩
    specialize hxr L hLs
    refine (StrongDual.norm_toLpₗ_le L).trans ?_
    gcongr

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ ∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ = ∫ (a : E), ‖L₁‖ * ‖L₂‖ * ‖a‖ ^ 2 ∂μ

Tactic:
congr with x

Goal state after:
case e_f
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
x : E
⊢ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ = ‖L₁‖ * ‖L₂‖ * ‖x‖ ^ 2
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case zero
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
⊢ μ {x | a < ‖x‖} = μ {a_1 | ‖a_1‖ ≤ a}ᶜ

Tactic:
congr with x

Goal state after:
case zero.e_6
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
c : ℝ≥0∞ := ⋯
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
x : E
⊢ a < ‖x‖ ↔ x ∉ {a_1 | ‖a_1‖ ≤ a}
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
n : ℕ
hn : μ {x | normThreshold a n < ‖x‖} ≤ μ {x | ‖x‖ ≤ a} * ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ n
h_mul_le : c * μ {x | normThreshold a (n + 1) < ‖x‖} ≤ μ {x | normThreshold a n < ‖x‖} ^ 2
⊢ μ {x | normThreshold a (n + 1) < ‖x‖} = c⁻¹ * (c * μ {x | normThreshold a (n + 1) < ‖x‖})

Tactic:
rw [← mul_assoc, ENNReal.inv_mul_cancel hc_pos.ne' hc_lt_top.ne, one_mul]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : IsGaussian μ
inst✝ : SecondCountableTopology E
L : StrongDual ℝ E
⊢ ∫ (x : E), ∫ (y : E), L x + L y ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ ∂μ =
    ∫ (x : E), L x + ∫ (y : E), L y ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ ∂μ

Tactic:
congr with x

Goal state after:
case e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : IsGaussian μ
inst✝ : SecondCountableTopology E
L : StrongDual ℝ E
x : E
⊢ ∫ (y : E), L x + L y ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ =
    L x + ∫ (y : E), L y ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
L : StrongDual ℝ E
this : (⇑L ∘ fun x ↦ ∑ i, x i • (stdOrthonormalBasis ℝ E) i) = ∑ i, fun x ↦ L ((stdOrthonormalBasis ℝ E) i) * x i
⊢ ∑ i, Var[HMul.hMul (L ((stdOrthonormalBasis ℝ E) i)); gaussianReal 0 1] = ‖L‖ ^ 2

Tactic:
change ∑ i, Var[fun x ↦ _ * (id x); gaussianReal 0 1] = _

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
L : StrongDual ℝ E
this : (⇑L ∘ fun x ↦ ∑ i, x i • (stdOrthonormalBasis ℝ E) i) = ∑ i, fun x ↦ L ((stdOrthonormalBasis ℝ E) i) * x i
⊢ ∑ i, Var[fun x ↦ L ((stdOrthonormalBasis ℝ E) i) * id x; gaussianReal 0 1] = ‖L‖ ^ 2
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case hx.refine_1
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 0 < c.toReal

pp: case hx.refine_2
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 0 < (1 - c).toReal

Tactic:
· rw [ENNReal.toReal_pos_iff]
      exact ⟨lt_trans (by norm_num) hc, h.trans_lt (by finiteness)⟩

Goal state after:
case hx.refine_2
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 0 < (1 - c).toReal
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
⊢ μ (closedBall 0 a) * ENNReal.ofReal (rexp (logRatio c')) = μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))

Tactic:
congr with x

Goal state after:
case e_a.e_6
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
x : E
⊢ x ∈ closedBall 0 a ↔ x ∈ {x | ‖x‖ ≤ a}
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ gaussianReal (∫ (x : EuclideanSpace ℝ ι), (EuclideanSpace.proj i) x ∂multivariateGaussian μ S)
      Var[⇑(EuclideanSpace.proj i); multivariateGaussian μ S].toNNReal =
    gaussianReal (μ.ofLp i) (S i i).toNNReal

Tactic:
ContinuousLinearMap.integral_comp_id_comm

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ gaussianReal ((EuclideanSpace.proj i) (∫ (x : EuclideanSpace ℝ ι), x ∂multivariateGaussian μ S))
      Var[⇑(EuclideanSpace.proj i); multivariateGaussian μ S].toNNReal =
    gaussianReal (μ.ofLp i) (S i i).toNNReal

case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ Integrable id (multivariateGaussian μ S)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s : ↥I
⊢ Measure.map (fun x ↦ x s) (projectiveFamily I) = gaussianReal 0 ↑s

Tactic:
by
    rw [(IsGaussian.hasGaussianLaw_id.eval s).map_eq_gaussianReal,
      integral_eval_projectiveFamily,
      variance_eval_projectiveFamily, Real.toNNReal_coe]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: case hm
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ ∫ (x : EuclideanSpace ℝ ↥J), x ∂Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S) =
    (EuclideanSpace.restrict₂ hJI) μ

Tactic:
ContinuousLinearMap.integral_id_map,

Goal state after:
case hm
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ (EuclideanSpace.restrict₂ hJI) (∫ (x : EuclideanSpace ℝ ↥I), x ∂multivariateGaussian μ S) =
    (EuclideanSpace.restrict₂ hJI) μ

case hm.h
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ Integrable id (multivariateGaussian μ S)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
ha : ¬μ {x | ‖x‖ ≤ a} = 1
ha_lt : μ {x | ‖x‖ ≤ a} < 1
hc'_lt : c' < 1
x : E
⊢ x ∈ Set.univ ↔ x ∈ closedBall 0 a ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n)

Tactic:
simp only [Set.mem_univ, Set.mem_union, Metric.mem_closedBall, dist_zero_right, Set.mem_iUnion,
      Set.mem_sdiff, not_le, true_iff]

Goal state after:
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
ha : ¬μ {x | ‖x‖ ≤ a} = 1
ha_lt : μ {x | ‖x‖ ≤ a} < 1
hc'_lt : c' < 1
x : E
⊢ ‖x‖ ≤ a ∨ ∃ i, ‖x‖ ≤ t (i + 1) ∧ t i < ‖x‖