mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), ‖f (n + 1) ω - f n ω‖ ≤ ↑R
h₀ : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω

Tactic:
refine ae_all_iff.2 fun n => condExp_nonneg ?_

Goal state after:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), ‖f (n + 1) ω - f n ω‖ ≤ ↑R
h₀ : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
n : ℕ
⊢ 0 ≤ᵐ[μ] f (n + 1) - f n
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
⊢ MemLp (stoppedProcess u τ n) p μ

Tactic:
rw [stoppedProcess_eq_of_mem_finset n hbdd]
  refine MemLp.add ?_ ?_
  · exact MemLp.indicator (ℱ.le n {a : Ω | n ≤ τ a} (hτ.measurableSet_ge n)) (hu n)
  · suffices MemLp (fun ω => ∑ i ∈ s with i < n, {a : Ω | τ a = i}.indicator (u i) ω) p μ by
      convert! this using 1; ext1 ω; simp only [Finset.sum_apply]
    refine memLp_finsetSum _ fun i _ => MemLp.indicator ?_ (hu i)
    exact ℱ.le i {a : Ω | τ a = i} (hτ.measurableSet_eq i)

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
⊢ complexMGF X μ = complexMGF Y μ'

Tactic:
by
  rw [← complexMGF_id_map h.aemeasurable_fst, ← complexMGF_id_map h.aemeasurable_snd, h.map_eq]

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : v ≠ 0
x : ℝ
⊢ x ∈ Function.support (gaussianPDF μ v)

Tactic:
exact (gaussianPDF_pos _ hv x).ne'

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst✝ : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
⊢ integrableExpSet X μ = integrableExpSet Y μ'

Tactic:
by
  refine integrableExpSet_eq_of_mgf' hXY ?_
  simp only [IsProbabilityMeasure.ne_zero, false_iff]
  suffices mgf Y μ' 0 ≠ 0 by
    intro h_contra
    simp [h_contra] at this
  rw [← hXY]
  exact (mgf_pos (by simp)).ne'

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

Goal state before:
pp: μ : ℝ
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 : ℝ
this : |c⁻¹| * |c| = 1
⊢ 1 * gaussianPDFReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v) x = gaussianPDFReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v) x

Tactic:
one_mul

Goal state after:
μ : ℝ
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 : ℝ
this : |c⁻¹| * |c| = 1
⊢ 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
⊢ 1 * cexp (-↑μ ^ 2 / (2 * ↑↑v) - (z + ↑μ / ↑↑v) ^ 2 / (4 * -↑↑(2 * v)⁻¹)) = cexp (z * ↑μ + ↑↑v * z ^ 2 / 2)

Tactic:
one_mul

Goal state after:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ cexp (-↑μ ^ 2 / (2 * ↑↑v) - (z + ↑μ / ↑↑v) ^ 2 / (4 * -↑↑(2 * v)⁻¹)) = cexp (z * ↑μ + ↑↑v * z ^ 2 / 2)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
z : ℂ
⊢ complexMGF id (gaussianReal μ v) z = cexp (z * ↑μ + ↑↑v * z ^ 2 / 2)

Tactic:
by
  by_cases hv : v = 0
  · simp [complexMGF, hv]
  calc ∫ x, cexp (z * x) ∂gaussianReal μ v
    _ = ∫ x, gaussianPDFReal μ v x * cexp (z * x) ∂ℙ := by
      simp_rw [integral_gaussianReal_eq_integral_smul hv, Complex.real_smul]
    _ = (√(2 * π * v))⁻¹
        * ∫ x : ℝ, cexp (-(2 * v)⁻¹ * x ^ 2 + (z + μ / v) * x + -μ ^ 2 / (2 * v)) ∂ℙ := by
      unfold gaussianPDFReal
      push_cast
      simp_rw [mul_assoc, integral_const_mul, ← Complex.exp_add]
      congr with x
      congr 1
      ring
    _ = (√(2 * π * v))⁻¹ * (π / - -(2 * v)⁻¹) ^ (1 / 2 : ℂ)
        * cexp (-μ ^ 2 / (2 * v) - (z + μ / v) ^ 2 / (4 * -(2 * v)⁻¹)) := by
      rw [integral_cexp_quadratic (by simpa using pos_iff_ne_zero.mpr hv), ← mul_assoc]
    _ = 1 * cexp (-μ ^ 2 / (2 * v) - (z + μ / v) ^ 2 / (4 * -(2 * v)⁻¹)) := by
      congr 1
      simp only [field, sqrt_eq_rpow, one_div, ofReal_inv, NNReal.coe_inv, NNReal.coe_mul,
        NNReal.coe_ofNat, ofReal_mul, ofReal_ofNat, neg_neg, div_inv_eq_mul,
        ne_eq, ofReal_eq_zero, rpow_eq_zero, not_false_eq_true]
      rw [Complex.ofReal_cpow (by positivity)]
      push_cast
      ring_nf
    _ = cexp (z * μ + v * z ^ 2 / 2) := by
      rw [one_mul]
      congr 1
      have : (v : ℂ) ≠ 0 := by simpa
      simp [field]
      ring

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : CompleteSpace E
hμ : MemLp id 2 μ
x : E
⊢ (covarianceOperator μ) x = ∫ (y : E), ⟪x, y⟫ • y ∂μ

Tactic:
by
  refine (unique_continuousLinearMapOfBilin _ fun y ↦ ?_).symm
  rw [real_inner_comm, ← integral_inner]
  · simp_rw [inner_smul_right, ← continuousLinearMapOfBilin_apply, ← covarianceOperator_inner hμ]
    rfl
  exact memLp_one_iff_integrable.1 <| hμ.smul (hμ.const_inner x)

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
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
x : E
hxL₁ : ↑↑(MemLp.toLp (fun x ↦ L₁ x) ⋯) x = L₁ x
hxL₂ : ↑↑(MemLp.toLp (fun x ↦ L₂ x) ⋯) x = L₂ x
⊢ ↑↑(MemLp.toLp ⇑L₂ ⋯) x * ↑↑(MemLp.toLp ⇑L₁ ⋯) x = L₁ x * L₂ x

Tactic:
hxL₁,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
x : E
hxL₁ : ↑↑(MemLp.toLp (fun x ↦ L₁ x) ⋯) x = L₁ x
hxL₂ : ↑↑(MemLp.toLp (fun x ↦ L₂ x) ⋯) x = L₂ x
⊢ ↑↑(MemLp.toLp ⇑L₂ ⋯) x * L₁ x = L₁ x * L₂ x
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case neg.inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this✝ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
⊢ ‖c‖ ^ ↑p ≤ 2 * ‖c‖ ^ (↑p - 1) * ‖y‖ + 2 ^ ↑p * ‖y - c‖ ^ ↑p

Tactic:
rcases le_total ‖y‖ (‖c‖ / 2)

Goal state after:
case neg.inr.inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this✝ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
h✝ : ‖y‖ ≤ ‖c‖ / 2
⊢ ‖c‖ ^ ↑p ≤ 2 * ‖c‖ ^ (↑p - 1) * ‖y‖ + 2 ^ ↑p * ‖y - c‖ ^ ↑p

case neg.inr.inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this✝ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
h✝ : ‖c‖ / 2 ≤ ‖y‖
⊢ ‖c‖ ^ ↑p ≤ 2 * ‖c‖ ^ (↑p - 1) * ‖y‖ + 2 ^ ↑p * ‖y - c‖ ^ ↑p
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‖} = 1 * μ {x | normThreshold a (n + 1) < ‖x‖}

Tactic:
one_mul

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_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‖} = μ {x | normThreshold a (n + 1) < ‖x‖}
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 : Fin (finrank ℝ E)), MemLp (HMul.hMul (L ((stdOrthonormalBasis ℝ E) i))) 2 (gaussianReal 0 1)

Tactic:
· exact fun i ↦ IsGaussian.memLp_two_id.const_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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[⇑L; μ] ≠ 0
⊢ μ {x} = 0

Tactic:
have hL_zero : μ.map L {L x} = 0 := by
      have : NullSingletonClass (μ.map L) := by
        rw [map_eq_gaussianReal L]
        refine nullSingletonClass_gaussianReal ?_
        simp only [ne_eq, Real.toNNReal_eq_zero, not_le]
        exact lt_of_le_of_ne (variance_nonneg _ _) hL.symm
      rw [measure_singleton]

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[⇑L; μ] ≠ 0
hL_zero : (Measure.map (⇑L) μ) {L x} = 0
⊢ μ {x} = 0
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ Measure.map X P = gaussianReal (∫ (x : Ω), X x ∂P) Var[X; P].toNNReal

Tactic:
rw [h.isGaussian_map.eq_gaussianReal (.map _ _), integral_map, variance_map]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ gaussianReal (∫ (x : Ω), id (X x) ∂P) Var[id ∘ X; P].toNNReal = gaussianReal (∫ (x : Ω), X x ∂P) Var[X; P].toNNReal

case hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ AEMeasurable id (Measure.map X P)

case hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ AEMeasurable X P

case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ AEMeasurable X P

case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ AEStronglyMeasurable id (Measure.map X P)
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ ⟪x, (toEuclideanCLM (CFC.sqrt S * CFC.sqrt S)) y⟫ = x.ofLp ⬝ᵥ S *ᵥ y.ofLp

pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ IsSelfAdjoint (toEuclideanCLM (CFC.sqrt S))

pp: case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ MemLp id 2 (stdGaussian (EuclideanSpace ℝ ι))

Tactic:
CFC.sqrt_mul_sqrt_self _ hS.nonneg,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ ⟪x, (toEuclideanCLM S) y⟫ = x.ofLp ⬝ᵥ S *ᵥ y.ofLp

ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ IsSelfAdjoint (toEuclideanCLM (CFC.sqrt S))

case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ MemLp id 2 (stdGaussian (EuclideanSpace ℝ ι))
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
this : covMatrix I = Matrix.of fun s t ↦ ℙ.real (Icc 0 ↑↑s ∩ Icc 0 ↑↑t)
⊢ (Matrix.of fun s t ↦ ℙ.real (Icc 0 ↑↑s ∩ Icc 0 ↑↑t)).PosSemidef

Tactic:
exact posSemidef_matrix_measure_inter (fun _ ↦ measurableSet_Icc)
    (fun _ ↦ isCompact_Icc.measure_ne_top)

Goal state after:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s : ↥I
⊢ AEMeasurable (fun x ↦ x s) (projectiveFamily I)

Tactic:
exact aemeasurable_id.eval s

Goal state after:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case hY
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x t) 2 (projectiveFamily I)

pp: I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)

Tactic:
· exact (IsGaussian.hasGaussianLaw_id.eval t).memLp_two

Goal state after:
I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case h₂
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 : ℕ → ℝ := ⋯
c : ℝ≥0∞ := ⋯
C : ℝ := ⋯
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
h_iUnion : Set.univ = closedBall 0 a ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n)
this :
  ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ +
      ∑' (i : ℕ), ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ
⊢ ∑' (i : ℕ), ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    c * ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ n))

Tactic:
← ENNReal.tsum_mul_left

Goal state after:
case h₂
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
h_iUnion : Set.univ = closedBall 0 a ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n)
this :
  ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ +
      ∑' (i : ℕ), ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ
⊢ ∑' (i : ℕ), ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    ∑' (i : ℕ), c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ i))
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: T : Type u_1
inst✝¹ : LinearOrder T
I : Finset T
inst✝ : OrderBot T
i j : Fin (#I + 1)
hij : i ≤ j
⊢ I.orderEmbOfFinWithBot i ≤ I.orderEmbOfFinWithBot j

Tactic:
obtain rfl | hi := eq_or_ne i 0

Goal state after:
case inl
T : Type u_1
inst✝¹ : LinearOrder T
I : Finset T
inst✝ : OrderBot T
j : Fin (#I + 1)
hij : 0 ≤ j
⊢ I.orderEmbOfFinWithBot 0 ≤ I.orderEmbOfFinWithBot j

case inr
T : Type u_1
inst✝¹ : LinearOrder T
I : Finset T
inst✝ : OrderBot T
i j : Fin (#I + 1)
hij : i ≤ j
hi : i ≠ 0
⊢ I.orderEmbOfFinWithBot i ≤ I.orderEmbOfFinWithBot j
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
h₁ : L₁.toBilinForm.IsPosSemidef
h₂ : L₂.toBilinForm.IsPosSemidef
x : StrongDual ℝ (E × F)
⊢ 0 ≤ ((L₁.diagonalStrongDualProd L₂).toBilinForm x) x

Tactic:
rw [toBilinForm_diagonalStrongDualProd_apply]

Goal state after:
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
h₁ : L₁.toBilinForm.IsPosSemidef
h₂ : L₂.toBilinForm.IsPosSemidef
x : StrongDual ℝ (E × F)
⊢ 0 ≤ (L₁.toBilinForm (x ∘SL inl ℝ E F)) (x ∘SL inl ℝ E F) + (L₂.toBilinForm (x ∘SL inr ℝ E F)) (x ∘SL inr ℝ E F)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
x✝ : MeasurableSpace β
f : α × β → StieltjesFunction ℝ
κ : Kernel α (β × ℝ)
ν : Kernel α β
hf : IsCondKernelCDF f κ ν
p : α × β
x : ℝ
⊢ (f p).measure (Iic x) = ENNReal.ofReal (↑(f p) x)

Tactic:
(f p).measure_Iic (hf.tendsto_atBot_zero p)

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
x✝ : MeasurableSpace β
f : α × β → StieltjesFunction ℝ
κ : Kernel α (β × ℝ)
ν : Kernel α β
hf : IsCondKernelCDF f κ ν
p : α × β
x : ℝ
⊢ ENNReal.ofReal (↑(f p) x - 0) = ENNReal.ofReal (↑(f p) x)
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ ((ξ ×ₖ prodMkLeft β η ∘ₖ (κ ×ₖ deterministic f hf)) ω) s =
    ((ξ ∘ₖ (κ ×ₖ deterministic f hf) ×ₖ (η ∘ₖ deterministic f hf)) ω) s

Tactic:
rw [prod_apply' _ _ _ hs, comp_apply' _ _ _ hs, lintegral_prod_deterministic,
    lintegral_comp, lintegral_prod_deterministic]

Goal state after:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ ∫⁻ (b : β), ((ξ ×ₖ prodMkLeft β η) (b, f ω)) s ∂κ ω =
    ∫⁻ (b : β), ∫⁻ (c : δ), ((η ∘ₖ deterministic f hf) ω) (Prod.mk c ⁻¹' s) ∂ξ (b, f ω) ∂κ ω

case hg
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable fun b ↦ ∫⁻ (c : δ), ((η ∘ₖ deterministic f hf) ω) (Prod.mk c ⁻¹' s) ∂ξ b

case hg
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable fun b ↦ ((η ∘ₖ deterministic f hf) ω) (Prod.mk b ⁻¹' s)

case hg
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable fun b ↦ ((ξ ×ₖ prodMkLeft β η) b) s