awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
hf : ∀ᵐ (x : ℝ), Membership.mem (γ := Set ℝ) (Ici 0) x → 0 x ≤ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ici 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
rw [EventuallyLE, ae_restrict_iff' measurableSet_Ici]

Premises used: MeasureTheory.ae_restrict_iff', Filter.EventuallyLE, measurableSet_Ici
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
x : ℝ
hx : 0 ≤ x
⊢ 0 x ≤ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ∀ᵐ (x : ℝ), Membership.mem (γ := Set ℝ) (Ici 0) x → 0 x ≤ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
exact ae_of_all _ (fun x (hx : 0 ≤ x) ↦ by positivity)

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
hfm :
  gammaPDFReal a r =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ici 0))] fun (x : ℝ) ↦
    r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) (Measure.restrict volume (Ici 0))

Tactic:
apply (measurable_gammaPDFReal a r).aestronglyMeasurable.congr

Premises used: MeasureTheory.AEStronglyMeasurable.congr, Measurable.aestronglyMeasurable, ProbabilityTheory.measurable_gammaPDFReal
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ gammaPDFReal a r =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ici 0))] fun (x : ℝ) ↦
    r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
(ae_restrict_iff' measurableSet_Ici).mpr <| ae_of_all _ fun x (hx : 0 ≤ x) ↦ ?_

Premises used: Iff.mpr, Filter.EventuallyEq, MeasureTheory.ae_of_all, MeasureTheory.ae_restrict_iff', measurableSet_Ici
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
hfm : ∀ (x : ℝ) (hx : 0 ≤ x), gammaPDFReal a r x = (fun (x : ℝ) ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) x
⊢ gammaPDFReal a r =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ici 0))] fun (x : ℝ) ↦
    r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
refine (ae_restrict_iff' measurableSet_Ici).mpr <| ae_of_all _ fun x (hx : 0 ≤ x) ↦ ?_

Premises used: Iff.mpr, MeasureTheory.ae_of_all, MeasureTheory.ae_restrict_iff', measurableSet_Ici
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
x : ℝ
hx : 0 ≤ x
hfm hfm₁ : gammaPDFReal a r x = r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
hfm₂ :
  (if 0 ≤ x then r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)) else 0) =
    r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
hfm₃ :
  (if True then r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)) else 0) =
    r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
⊢ gammaPDFReal a r x = (fun (x : ℝ) ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) x

Tactic:
simp_rw [gammaPDFReal, eq_true_intro hx, ite_true]

Premises used: ProbabilityTheory.gammaPDFReal, eq_true_intro, ite_true
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ Eq (α := ℝ≥0∞) ((gammaMeasure a r : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp [gammaMeasure, lintegral_gammaPDF_eq_one ha hr]

Premises used: ProbabilityTheory.gammaMeasure, ProbabilityTheory.lintegral_gammaPDF_eq_one
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
⊢ IsProbabilityMeasure (gammaMeasure a r)

Tactic:
have : IsProbabilityMeasure (gammaMeasure a r) := isProbabilityMeasure_gammaMeasure ha hr
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
rw :
  (∫⁻ (a_1 : ℝ) in Iic x, gammaPDF a r a_1).toReal =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic x)) fun (x : ℝ) ↦ gammaPDFReal a r x
⊢ (↑(cdf (gammaMeasure a r)) : ℝ → ℝ) x =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic x)) fun (x : ℝ) ↦ gammaPDFReal a r x

Tactic:
rw [cdf_eq_real, gammaMeasure, measureReal_def, withDensity_apply _ measurableSet_Iic]

Premises used: ProbabilityTheory.gammaMeasure, ProbabilityTheory.cdf_eq_real, measurableSet_Iic, MeasureTheory.measureReal_def, MeasureTheory.withDensity_apply
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ (∫⁻ (a_1 : ℝ) in Iic x, gammaPDF a r a_1).toReal =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic x)) fun (x : ℝ) ↦ gammaPDFReal a r x

Tactic:
(integral_eq_lintegral_of_nonneg_ae ?_ ?_).symm

Premises used: ProbabilityTheory.gammaPDF, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, Eq.symm
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
refine_1 : 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Iic x))] gammaPDFReal a r
refine_2 :
  AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gammaPDFReal a r) (Measure.restrict volume (Iic x))
⊢ (∫⁻ (a_1 : ℝ) in Iic x, gammaPDF a r a_1).toReal =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic x)) fun (x : ℝ) ↦ gammaPDFReal a r x

Tactic:
refine (integral_eq_lintegral_of_nonneg_ae ?_ ?_).symm

Premises used: MeasureTheory.integral_eq_lintegral_of_nonneg_ae, Eq.symm
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
b : ℝ
⊢ 0 b ≤ gammaPDFReal a r b

Tactic:
simp [gammaPDFReal_nonneg ha hr]

Premises used: ProbabilityTheory.gammaPDFReal_nonneg
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Iic x))] gammaPDFReal a r

Tactic:
exact ae_of_all _ fun b ↦ by simp [gammaPDFReal_nonneg ha hr]

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gammaPDFReal a r) (Measure.restrict volume (Iic x))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
simp : (gammaMeasure a r).real (Iic x) = (∫⁻ (x : ℝ) in Iic x, ENNReal.ofReal (gammaPDFReal a r x)).toReal
⊢ (↑(cdf (gammaMeasure a r)) : ℝ → ℝ) x = (∫⁻ (x : ℝ) in Iic x, gammaPDF a r x).toReal

Tactic:
simp only [gammaPDF, cdf_eq_real]

Premises used: ProbabilityTheory.gammaPDF, ProbabilityTheory.cdf_eq_real
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ (gammaMeasure a r).real (Iic x) = (∫⁻ (x : ℝ) in Iic x, ENNReal.ofReal (gammaPDFReal a r x)).toReal

Tactic:
simp [gammaMeasure, gammaPDF, measureReal_def]

Premises used: ProbabilityTheory.gammaMeasure, ProbabilityTheory.gammaPDF, MeasureTheory.measureReal_def
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_3 : IsGaussian μ
⊢ Eq (α := ℝ≥0∞) ((Measure.map (⇑0 : (a : E) → ℝ) μ : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp [IsGaussian.map_eq_gaussianReal]

Premises used: ProbabilityTheory.IsGaussian.map_eq_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_3 : IsGaussian μ
⊢ Eq (α := ℝ≥0∞) ((Measure.map (⇑0 : (a : E) → ℝ) μ : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
have : μ.map (0 : StrongDual ℝ E) Set.univ = 1 := by simp [IsGaussian.map_eq_gaussianReal]
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_3 : IsGaussian μ
this : Eq (α := ℝ≥0∞) ((Measure.map (⇑0 : (a : E) → ℝ) μ : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Measurable.{u_1, 0} (α := E) (β := ℝ) (⇑0 : (a : E) → ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_3 : IsGaussian μ
this : Eq (α := ℝ≥0∞) ((Measure.map (⇑0 : (a : E) → ℝ) μ : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simpa [Measure.map_apply (by fun_prop : Measurable (0 : StrongDual ℝ E)) .univ] using this

Premises used: MeasureTheory.Measure.map_apply, MeasurableSet.univ
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
rw :
  gaussianReal ((L : (a : ℝ) → ℝ) m) ((HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v) =
    gaussianReal (∫ (x : ℝ), (L : (a : ℝ) → ℝ) x ∂gaussianReal m v) Var[(⇑L : (a : ℝ) → ℝ); gaussianReal m v].toNNReal
⊢ Measure.map (⇑L : (a : ℝ) → ℝ) (gaussianReal m v) =
    gaussianReal (∫ (x : ℝ), (L : (a : ℝ) → ℝ) x ∂gaussianReal m v) Var[(⇑L : (a : ℝ) → ℝ); gaussianReal m v].toNNReal

Tactic:
rw [gaussianReal_map_continuousLinearMap]

Premises used: ProbabilityTheory.gaussianReal_map_continuousLinearMap
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
simp :
  gaussianReal ((L : (a : ℝ) → ℝ) m) ((HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v) =
    gaussianReal ((L : (a : ℝ) → ℝ) m)
      (max (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) 0 * (↑v : ℝ)).toNNReal
⊢ gaussianReal ((L : (a : ℝ) → ℝ) m) ((HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v) =
    gaussianReal (∫ (x : ℝ), (L : (a : ℝ) → ℝ) x ∂gaussianReal m v) Var[(⇑L : (a : ℝ) → ℝ); gaussianReal m v].toNNReal

Tactic:
simp only [integral_continuousLinearMap_gaussianReal, variance_continuousLinearMap_gaussianReal,
      Real.coe_toNNReal']

Premises used: ProbabilityTheory.integral_continuousLinearMap_gaussianReal, Real.coe_toNNReal', ProbabilityTheory.variance_continuousLinearMap_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
e_v :
  (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v =
    (max (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) 0 * (↑v : ℝ)).toNNReal
⊢ gaussianReal ((L : (a : ℝ) → ℝ) m) ((HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v) =
    gaussianReal ((L : (a : ℝ) → ℝ) m)
      (max (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) 0 * (↑v : ℝ)).toNNReal

Tactic:
congr
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ 0 ≤ max (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) 0

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
e_v :
  (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v =
    (max (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) 0).toNNReal * v
⊢ (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v =
    (max (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) 0 * (↑v : ℝ)).toNNReal

Tactic:
rw [Real.toNNReal_mul (by positivity), Real.toNNReal_coe]

Premises used: Real.toNNReal_mul, Real.toNNReal_coe
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
e_v :
  HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2 =
    max (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) 0
⊢ (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v =
    (max (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) 0).toNNReal * v

Tactic:
congr
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
e_v : 0 ≤ HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2
⊢ HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2 =
    max (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) 0

Tactic:
simp only [left_eq_sup]

Premises used: left_eq_sup
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ 0 ≤ HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
μ : Measure ℝ
h : IsGaussian μ
⊢ μ = Measure.map (⇑(ContinuousLinearMap.id ℝ ℝ) : (a : ℝ) → ℝ) μ

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
μ : Measure ℝ
h : IsGaussian μ
rw :
  gaussianReal (∫ (x : ℝ), (ContinuousLinearMap.id ℝ ℝ : (a : ℝ) → ℝ) x ∂μ)
      Var[(⇑(ContinuousLinearMap.id ℝ ℝ) : (a : ℝ) → ℝ); μ].toNNReal =
    gaussianReal (∫ (x : ℝ), id x ∂μ) Var[id; μ].toNNReal
⊢ Measure.map (⇑(ContinuousLinearMap.id ℝ ℝ) : (a : ℝ) → ℝ) μ = gaussianReal (∫ (x : ℝ), id x ∂μ) Var[id; μ].toNNReal

Tactic:
rw [h.map_eq_gaussianReal]

Premises used: ProbabilityTheory.IsGaussian.map_eq_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
μ : Measure ℝ
h : IsGaussian μ
⊢ gaussianReal (∫ (x : ℝ), (ContinuousLinearMap.id ℝ ℝ : (a : ℝ) → ℝ) x ∂μ)
      Var[(⇑(ContinuousLinearMap.id ℝ ℝ) : (a : ℝ) → ℝ); μ].toNNReal =
    gaussianReal (∫ (x : ℝ), id x ∂μ) Var[id; μ].toNNReal

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), IsGaussian (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
⊢ IsGaussian μ

Tactic:
⟨fun L ↦ ?_⟩

Premises used: ProbabilityTheory.IsGaussian.mk
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), IsGaussian (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
refine :
  ∀ (L : StrongDual ℝ E),
    Measure.map (⇑L : (a : E) → ℝ) μ =
      gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal
⊢ IsGaussian μ

Tactic:
refine ⟨fun L ↦ ?_⟩
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), IsGaussian (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
L : StrongDual ℝ E
rw :
  gaussianReal (∫ (x : E), id ((L : (a : E) → ℝ) x) ∂μ) Var[id ∘ (⇑L : (a : E) → ℝ); μ].toNNReal =
    gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal
hX : AEMeasurable (α := ℝ) (_m := Real.measurableSpace) id (Measure.map (⇑L : (a : E) → ℝ) μ)
hY hφ : AEMeasurable (β := ℝ) (⇑L : (a : E) → ℝ) μ
hfm : AEStronglyMeasurable (α := ℝ) (m₀ := Real.measurableSpace) id (Measure.map (⇑L : (a : E) → ℝ) μ)
⊢ Measure.map (⇑L : (a : E) → ℝ) μ =
    gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal

Tactic:
rw [(h L).eq_gaussianReal, integral_map, variance_map]

Premises used: MeasureTheory.integral_map, ProbabilityTheory.variance_map, ProbabilityTheory.IsGaussian.eq_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), IsGaussian (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
L : StrongDual ℝ E
⊢ gaussianReal (∫ (x : E), id ((L : (a : E) → ℝ) x) ∂μ) Var[id ∘ (⇑L : (a : E) → ℝ); μ].toNNReal =
    gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), IsGaussian (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
L : StrongDual ℝ E
⊢ AEMeasurable (α := ℝ) (_m := Real.measurableSpace) id (Measure.map (⇑L : (a : E) → ℝ) μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), IsGaussian (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
L : StrongDual ℝ E
⊢ AEMeasurable (β := ℝ) (⇑L : (a : E) → ℝ) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), IsGaussian (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
L : StrongDual ℝ E
⊢ AEStronglyMeasurable (α := ℝ) (m₀ := Real.measurableSpace) id (Measure.map (⇑L : (a : E) → ℝ) μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), ∃ (m : ℝ) (v : ℝ≥0), Measure.map (⇑L : (a : E) → ℝ) μ = gaussianReal m v
⊢ IsGaussian μ

Tactic:
isGaussian_of_isGaussian_map fun L ↦ ?_

Premises used: ProbabilityTheory.isGaussian_of_isGaussian_map
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), ∃ (m : ℝ) (v : ℝ≥0), Measure.map (⇑L : (a : E) → ℝ) μ = gaussianReal m v
refine : ∀ (L : E →L[ℝ] ℝ), IsGaussian (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
⊢ IsGaussian μ

Tactic:
refine isGaussian_of_isGaussian_map fun L ↦ ?_

Premises used: ProbabilityTheory.isGaussian_of_isGaussian_map
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), ∃ (m : ℝ) (v : ℝ≥0), Measure.map (⇑L : (a : E) → ℝ) μ = gaussianReal m v
L : E →L[ℝ] ℝ
obtain :
  ∀ (m : ℝ) (v : ℝ≥0) (h : Measure.map (⇑L : (a : E) → ℝ) μ = gaussianReal m v),
    IsGaussian (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
⊢ IsGaussian (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)

Tactic:
obtain ⟨m, v, h⟩ := h L
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
μ : Measure E
h_1 : ∀ (L : E →L[ℝ] ℝ), ∃ (m : ℝ) (v : ℝ≥0), Measure.map (⇑L : (a : E) → ℝ) μ = gaussianReal m v
L : E →L[ℝ] ℝ
m : ℝ
v : ℝ≥0
h : Measure.map (⇑L : (a : E) → ℝ) μ = gaussianReal m v
rw : IsGaussian (gaussianReal m v)
⊢ IsGaussian (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)

Tactic:
rw [h]
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
μ : Measure E
h_1 : ∀ (L : E →L[ℝ] ℝ), ∃ (m : ℝ) (v : ℝ≥0), Measure.map (⇑L : (a : E) → ℝ) μ = gaussianReal m v
L : E →L[ℝ] ℝ
m : ℝ
v : ℝ≥0
h : Measure.map (⇑L : (a : E) → ℝ) μ = gaussianReal m v
⊢ IsGaussian (gaussianReal m v)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
F : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid F
inst_5 : Module ℝ F
mF : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
μ : Measure E
L : E →L[ℝ] F
inst_7 : IsGaussian μ
hL : Measurable.{u_1, u_2} (α := E) (β := F) (⇑L : (a : E) → F)
⊢ IsGaussian.{u_2} (E := F) (mE := mF) (Measure.map (⇑L : (a : E) → F) μ)

Tactic:
isGaussian_of_map_eq_gaussianReal fun L' ↦ ⟨μ[L' ∘L L], Var[L' ∘L L; μ].toNNReal, ?_⟩

Premises used: ContinuousLinearMap.comp, ProbabilityTheory.variance, ProbabilityTheory.isGaussian_of_map_eq_gaussianReal, MeasureTheory.integral, Exists.intro, DFunLike.coe, Real.toNNReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
F : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid F
inst_5 : Module ℝ F
mF : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
μ : Measure E
L : E →L[ℝ] F
inst_7 : IsGaussian μ
hL : Measurable.{u_1, u_2} (α := E) (β := F) (⇑L : (a : E) → F)
refine :
  ∀ (L' : F →L[ℝ] ℝ),
    Measure.map (α := F) (⇑L' : (a : F) → ℝ) (Measure.map (⇑L : (a : E) → F) μ) =
      gaussianReal (∫ (x : E), (L' ∘SL L : (a : E) → ℝ) x ∂μ) Var[(⇑(L' ∘SL L) : (a : E) → ℝ); μ].toNNReal
⊢ IsGaussian.{u_2} (E := F) (mE := mF) (Measure.map (⇑L : (a : E) → F) μ)

Tactic:
refine isGaussian_of_map_eq_gaussianReal fun L' ↦ ⟨μ[L' ∘L L], Var[L' ∘L L; μ].toNNReal, ?_⟩

Premises used: ContinuousLinearMap.comp, ProbabilityTheory.variance, ProbabilityTheory.isGaussian_of_map_eq_gaussianReal, MeasureTheory.integral, Exists.intro, DFunLike.coe, Real.toNNReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
F : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid F
inst_5 : Module ℝ F
mF : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
μ : Measure E
L : E →L[ℝ] F
inst_7 : IsGaussian μ
hL : Measurable.{u_1, u_2} (α := E) (β := F) (⇑L : (a : E) → F)
L' : F →L[ℝ] ℝ
funProp : mF ≤ mF
funProp₁ : MeasurableEmbedding (β := ℝ) fun (a : F) ↦ (L' : (a : F) → ℝ) a
⊢ Measurable (α := F) (β := ℝ) (⇑L' : (a : F) → ℝ)

Tactic:
fun_prop