mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v - min (v - l) (u - v) / 2 ∈ Set.Ioo l u

Tactic:
constructor

Goal state after:
case left
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ l < v - min (v - l) (u - v) / 2

case right
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v - min (v - l) (u - v) / 2 < u
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case pos
μ : ℝ
v : ℝ≥0
c : ℝ
hv : v = 0
⊢ Measure.map (fun x ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)

pp: case neg
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
⊢ Measure.map (fun x ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)

Tactic:
· simp [hv, mul_zero, gaussianReal_zero_var]

Goal state after:
case neg
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
⊢ 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 e'_3.e'_2
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ (NNReal.mk (c ^ 2) ⋯)⁻¹ * v = NNReal.mk (c⁻¹ ^ 2) ⋯ * v

Tactic:
ext

Goal state after:
case e'_3.e'_2
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ ↑((NNReal.mk (c ^ 2) ⋯)⁻¹ * v) = ↑(NNReal.mk (c⁻¹ ^ 2) ⋯ * v)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
y : ℝ
⊢ (fun x ↦ y + -x) = (fun x ↦ y + x) ∘ fun x ↦ -x

Tactic:
ext

Goal state after:
μ : ℝ
v : ℝ≥0
y x✝ : ℝ
⊢ y + -x✝ = ((fun x ↦ y + x) ∘ fun x ↦ -x) x✝
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ (∫ (ω : Ω), X ω ^ 2 * rexp (v * X ω) ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2 =
    (∫ (ω : Ω), X ω ^ 2 * rexp (v * X ω) ∂μ - (2 * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
        deriv (cgf X μ) v ^ 2 * mgf X μ v) /
      mgf X μ v

Tactic:
by
    rw [add_div, sub_div, sub_add]
    congr 1
    rw [mul_div_cancel_right₀, deriv_cgf h]
    · ring
    · exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'

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

Goal state before:
pp: case neg.refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, xs n ∈ {t}ᶜ
hx_eq : ∀ (n : ℕ), complexMGF X μ ↑(xs n) = complexMGF Y μ' ↑(xs n)
⊢ Tendsto (fun n ↦ ↑(xs n)) atTop (𝓝 ↑t) ∧ ∀ᶠ (n : ℕ) in atTop, ↑(xs n) ∈ {↑t}ᶜ

Tactic:
constructor

Goal state after:
case neg.refine_1.left
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, xs n ∈ {t}ᶜ
hx_eq : ∀ (n : ℕ), complexMGF X μ ↑(xs n) = complexMGF Y μ' ↑(xs n)
⊢ Tendsto (fun n ↦ ↑(xs n)) atTop (𝓝 ↑t)

case neg.refine_1.right
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, xs n ∈ {t}ᶜ
hx_eq : ∀ (n : ℕ), complexMGF X μ ↑(xs n) = complexMGF Y μ' ↑(xs n)
⊢ ∀ᶠ (n : ℕ) in atTop, ↑(xs n) ∈ {↑t}ᶜ
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
h : ¬MemLp id 2 μ
⊢ covarianceBilin μ = 0

Tactic:
ext

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
μ : Measure E
h : ¬MemLp id 2 μ
x✝¹ x✝ : E
⊢ ((covarianceBilin μ) x✝¹) x✝ = (0 x✝¹) x✝
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ integrableExpSet id (gaussianReal μ v) = Set.univ

Tactic:
ext

Goal state after:
μ : ℝ
v : ℝ≥0
x✝ : ℝ
⊢ x✝ ∈ integrableExpSet id (gaussianReal μ v) ↔ x✝ ∈ Set.univ
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case neg
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 μ
⊢ covarianceBilin (Measure.map (fun x ↦ c + x) μ) = covarianceBilin μ

Tactic:
ext

Goal state after:
case neg
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✝¹ x✝ : E
⊢ ((covarianceBilin (Measure.map (fun x ↦ c + x) μ)) x✝¹) x✝ = ((covarianceBilin μ) x✝¹) x✝
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
inst✝ : IsProbabilityMeasure μ
c x✝¹ x✝ : E
h : MemLp (id ∘ fun x ↦ c + x) 2 μ
⊢ id = (fun x ↦ -c) + id ∘ fun x ↦ c + x

Tactic:
ext

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c x✝² x✝¹ : E
h : MemLp (id ∘ fun x ↦ c + x) 2 μ
x✝ : E
⊢ id x✝ = ((fun x ↦ -c) + id ∘ fun x ↦ c + x) x✝
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
L : StrongDual ℝ E
⊢ (⇑L ∘ fun x ↦ x + c) = fun x ↦ L x + L c

Tactic:
ext

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
L : StrongDual ℝ E
x✝ : E
⊢ (⇑L ∘ fun x ↦ x + c) x✝ = L x✝ + L c
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 y : E
⊢ ⟪∫ (y : E), ⟪x, y⟫ • y ∂μ, y⟫ =
    (((uncenteredCovarianceBilinDual μ).bilinearComp (toDualMap ℝ E).toContinuousLinearMap
          (toDualMap ℝ E).toContinuousLinearMap)
        x)
      y

Tactic:
real_inner_comm,

Goal state after:
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 y : E
⊢ ⟪y, ∫ (y : E), ⟪x, y⟫ • y ∂μ⟫ =
    (((uncenteredCovarianceBilinDual μ).bilinearComp (toDualMap ℝ E).toContinuousLinearMap
          (toDualMap ℝ E).toContinuousLinearMap)
        x)
      y
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
⊢ uncenteredCovarianceBilinDual 0 = 0

Tactic:
ext

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
x✝¹ x✝ : StrongDual ℝ E
⊢ ((uncenteredCovarianceBilinDual 0) x✝¹) x✝ = (0 x✝¹) x✝
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
p : ℝ≥0∞
h_Lp : MemLp (fun x ↦ x - ∫ (y : E), y ∂μ) p μ
⊢ id = fun x ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ

Tactic:
ext

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
p : ℝ≥0∞
h_Lp : MemLp (fun x ↦ x - ∫ (y : E), y ∂μ) p μ
x✝ : E
⊢ id x✝ = x✝ - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: 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 - 1) * ‖c‖ ≤ ‖c‖ ^ (↑p - 1) * (2 * ‖y‖)

Tactic:
by gcongr; linarith

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), L x ∂μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ = 0

Tactic:
rw [integral_conv (by fun_prop)]

Goal state after:
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 + y) ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ ∂μ = 0
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
n : StrongDual ℝ E → ℤ
h :
  ∀ (L : StrongDual ℝ E),
    ↑(n L) =
      (↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2 - ↑(L m) * I + ↑((f L) L) / 2) /
        (2 * ↑π * I)
this✝¹ : Continuous n
this✝ : ∀ (x : StrongDual ℝ E), n = Function.const (StrongDual ℝ E) (n x)
this : ∀ (L : StrongDual ℝ E), n L = 0
hn : ∀ (L : StrongDual ℝ E), ((covarianceBilinDual μ) L) L = (f L) L ∧ L (∫ (x : E), x ∂μ) = L m
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ

Tactic:
constructor

Goal state after:
case left
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
n : StrongDual ℝ E → ℤ
h :
  ∀ (L : StrongDual ℝ E),
    ↑(n L) =
      (↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2 - ↑(L m) * I + ↑((f L) L) / 2) /
        (2 * ↑π * I)
this✝¹ : Continuous n
this✝ : ∀ (x : StrongDual ℝ E), n = Function.const (StrongDual ℝ E) (n x)
this : ∀ (L : StrongDual ℝ E), n L = 0
hn : ∀ (L : StrongDual ℝ E), ((covarianceBilinDual μ) L) L = (f L) L ∧ L (∫ (x : E), x ∂μ) = L m
⊢ m = ∫ (x : E), x ∂μ

case right
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
n : StrongDual ℝ E → ℤ
h :
  ∀ (L : StrongDual ℝ E),
    ↑(n L) =
      (↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2 - ↑(L m) * I + ↑((f L) L) / 2) /
        (2 * ↑π * I)
this✝¹ : Continuous n
this✝ : ∀ (x : StrongDual ℝ E), n = Function.const (StrongDual ℝ E) (n x)
this : ∀ (L : StrongDual ℝ E), n L = 0
hn : ∀ (L : StrongDual ℝ E), ((covarianceBilinDual μ) L) L = (f L) L ∧ L (∫ (x : E), x ∂μ) = L m
⊢ f = covarianceBilinDual μ
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case e_a
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}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ n =
    ENNReal.ofReal (rexp (-Real.log (μ {x | ‖x‖ ≤ a} / (1 - μ {x | ‖x‖ ≤ a})).toReal * 2 ^ n))

Tactic:
rw [← Real.log_inv, mul_comm (Real.log _), ← Real.log_rpow (by positivity),
    Real.exp_log (by positivity), ← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity),
    ENNReal.toReal_div, inv_div, ← ENNReal.toReal_div, ENNReal.ofReal_toReal]

Goal state after:
case e_a
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}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ n = ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ n

case e_a
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}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ (1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a} ≠ ∞
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 : ∀ (L : StrongDual ℝ E), Var[⇑L; μ] = 0
L : StrongDual ℝ E
⊢ charFunDual μ L = charFunDual (Measure.dirac (∫ (x : E), x ∂μ)) L

Tactic:
charFunDual_dirac,

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 : ∀ (L : StrongDual ℝ E), Var[⇑L; μ] = 0
L : StrongDual ℝ E
⊢ charFunDual μ L = cexp (↑(L (∫ (x : E), x ∂μ)) * I)
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
  f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
    (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
this✝ : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((g L) L) / 2)
hg : g.toBilinForm.IsPosSemidef
this : m = ∫ (x : E), x ∂μ ∧ g = covarianceBilinDual μ
⊢ f = covarianceBilin μ

Tactic:
ext

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
  f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
    (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
this✝ : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((g L) L) / 2)
hg : g.toBilinForm.IsPosSemidef
this : m = ∫ (x : E), x ∂μ ∧ g = covarianceBilinDual μ
x✝¹ x✝ : E
⊢ (f x✝¹) x✝ = ((covarianceBilin μ) x✝¹) x✝
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i✝ j i : ι
⊢ (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫

Tactic:
ext

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i✝ j i : ι
x✝ : EuclideanSpace ℝ ι
⊢ x✝.ofLp i = ⟪(EuclideanSpace.basisFun ι ℝ) i, x✝⟫
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

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

Tactic:
ext

Goal state after:
I : Finset ℝ≥0
i✝ j✝ : ↥I
⊢ covMatrix I i✝ j✝ = Matrix.of (fun s t ↦ ℙ.real (Icc 0 ↑↑s ∩ Icc 0 ↑↑t)) i✝ j✝
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i✝ j i : ↥J
⊢ (fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis i, u⟫) ∘ ⇑(EuclideanSpace.restrict₂ hJI) = fun u ↦ u.ofLp ⟨↑i, ⋯⟩

Tactic:
ext

Goal state after:
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i✝ j i : ↥J
x✝ : EuclideanSpace ℝ ↥I
⊢ ((fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis i, u⟫) ∘ ⇑(EuclideanSpace.restrict₂ hJI)) x✝ = x✝.ofLp ⟨↑i, ⋯⟩
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : Fintype ι
E : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (fun ω x ↦ X x ω) P
⊢ ∑ i, X i = ⇑(∑ i, ContinuousLinearMap.proj i) ∘ fun ω x ↦ X x ω

Tactic:
ext

Goal state after:
Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : Fintype ι
E : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (fun ω x ↦ X x ω) P
x✝ : Ω
⊢ (∑ i, X i) x✝ = (⇑(∑ i, ContinuousLinearMap.proj i) ∘ fun ω x ↦ X x ω) x✝
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

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

Tactic:
exact (IsGaussian.hasGaussianLaw_id.eval s).memLp_two

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

Goal state before:
pp: I J : Finset ℝ≥0
hJI : J ⊆ I
⊢ projectiveFamily J = Measure.map (Finset.restrict₂ hJI) (projectiveFamily I)

Tactic:
projectiveFamily

Goal state after:
I J : Finset ℝ≥0
hJI : J ⊆ I
⊢ projectiveFamily J =
    Measure.map (Finset.restrict₂ hJI)
      (Measure.map (⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm) (multivariateGaussian 0 (covMatrix I)))
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I J : Finset ℝ≥0
hJI : J ⊆ I
⊢ Finset.restrict₂ hJI ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm = ofLp ∘ ⇑(EuclideanSpace.restrict₂ hJI)

Tactic:
ext

Goal state after:
I J : Finset ℝ≥0
hJI : J ⊆ I
x✝¹ : WithLp 2 (↥I → ℝ)
x✝ : ↥J
⊢ (Finset.restrict₂ hJI ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm) x✝¹ x✝ =
    (ofLp ∘ ⇑(EuclideanSpace.restrict₂ hJI)) x✝¹ x✝
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: case empty
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : ι → Ω → E
inst✝ : NormedSpace ℝ E
this : IsProbabilityMeasure P
mX : ∀ i ∈ ∅, AEMeasurable (X i) P
hX : iIndepFun (∅.restrict X) P
⊢ charFunDual (Measure.map (∑ i ∈ ∅, X i) P) = ∏ i ∈ ∅, charFunDual (Measure.map (X i) P)

Tactic:
ext

Goal state after:
case empty
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : ι → Ω → E
inst✝ : NormedSpace ℝ E
this : IsProbabilityMeasure P
mX : ∀ i ∈ ∅, AEMeasurable (X i) P
hX : iIndepFun (∅.restrict X) P
x✝ : StrongDual ℝ E
⊢ charFunDual (Measure.map (∑ i ∈ ∅, X i) P) x✝ = (∏ i ∈ ∅, charFunDual (Measure.map (X i) P)) x✝
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : T → Ω → E
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module ℝ E
hX : IsGaussianProcess X P
hXY : ∀ (t : T), X t =ᵐ[P] Y t
I : Finset T
⊢ HasGaussianLaw (fun ω ↦ I.restrict fun x ↦ Y x ω) P

Tactic:
constructor

Goal state after:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : T → Ω → E
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module ℝ E
hX : IsGaussianProcess X P
hXY : ∀ (t : T), X t =ᵐ[P] Y t
I : Finset T
⊢ IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ Y x ω) P)
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
x y : ↥(image t univ) → E
⊢ (fun i ↦ (x + y) ⟨t i.succ, ⋯⟩ - (x + y) ⟨t i.castSucc, ⋯⟩) =
    (fun i ↦ x ⟨t i.succ, ⋯⟩ - x ⟨t i.castSucc, ⋯⟩) + fun i ↦ y ⟨t i.succ, ⋯⟩ - y ⟨t i.castSucc, ⋯⟩

Tactic:
ext

Goal state after:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
x y : ↥(image t univ) → E
x✝ : Fin n
⊢ (x + y) ⟨t x✝.succ, ⋯⟩ - (x + y) ⟨t x✝.castSucc, ⋯⟩ =
    ((fun i ↦ x ⟨t i.succ, ⋯⟩ - x ⟨t i.castSucc, ⋯⟩) + fun i ↦ y ⟨t i.succ, ⋯⟩ - y ⟨t i.castSucc, ⋯⟩) x✝