awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
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)))
rw :
  (r ^ a / Gamma a *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        a_1 ^ (a - 1) * rexp (-(r * a_1))) =
    1
rw₁ : r ^ a / Gamma a * ((1 / r) ^ a * Gamma a) = 1
rw₂ : r ^ a * ((1 / r) ^ a * Gamma a) / Gamma a = 1
rw₃ : r ^ a * (1 / r) ^ a * Gamma a / Gamma a = 1
rw₄ : r ^ a * (1 / r) ^ a * (Gamma a / Gamma a) = 1
rw₅ : r ^ a * (1 / r) ^ a * 1 = 1
rw₆ : r ^ a * (1 / r) ^ a = 1
rw₇ : r ^ a * (HPow.hPow (α := ℝ) 1 a / r ^ a) = 1
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      r ^ a / Gamma a * (a_1 ^ (a - 1) * rexp (-(r * a_1))))
    1
have rw₈ : r ^ a * (1 / r ^ a) = 1
Tactic: rw [integral_const_mul, integral_rpow_mul_exp_neg_mul_Ioi ha hr, div_mul_eq_mul_div,
      ← mul_assoc, mul_div_assoc, div_self (Gamma_pos_of_pos ha).ne', mul_one,
      div_rpow zero_le_one hr.le, one_rpow, mul_one_div, div_self (rpow_pos_of_pos hr _).ne']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
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)))
rw :
  (r ^ a / Gamma a *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        a_1 ^ (a - 1) * rexp (-(r * a_1))) =
    1
rw₁ : r ^ a / Gamma a * ((1 / r) ^ a * Gamma a) = 1
rw₂ : r ^ a * ((1 / r) ^ a * Gamma a) / Gamma a = 1
rw₃ : r ^ a * (1 / r) ^ a * Gamma a / Gamma a = 1
rw₄ : r ^ a * (1 / r) ^ a * (Gamma a / Gamma a) = 1
rw₅ : r ^ a * (1 / r) ^ a * 1 = 1
rw₆ : r ^ a * (1 / r) ^ a = 1
rw₇ : r ^ a * (HPow.hPow (α := ℝ) 1 a / r ^ a) = 1
rw₈ : r ^ a * (1 / r ^ a) = 1
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      r ^ a / Gamma a * (a_1 ^ (a - 1) * rexp (-(r * a_1))))
    1
have rw₉ : r ^ a / r ^ a = 1
Tactic: rw [integral_const_mul, integral_rpow_mul_exp_neg_mul_Ioi ha hr, div_mul_eq_mul_div,
      ← mul_assoc, mul_div_assoc, div_self (Gamma_pos_of_pos ha).ne', mul_one,
      div_rpow zero_le_one hr.le, one_rpow, mul_one_div, div_self (rpow_pos_of_pos hr _).ne']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
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)))
rw :
  (r ^ a / Gamma a *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        a_1 ^ (a - 1) * rexp (-(r * a_1))) =
    1
rw₁ : r ^ a / Gamma a * ((1 / r) ^ a * Gamma a) = 1
rw₂ : r ^ a * ((1 / r) ^ a * Gamma a) / Gamma a = 1
rw₃ : r ^ a * (1 / r) ^ a * Gamma a / Gamma a = 1
rw₄ : r ^ a * (1 / r) ^ a * (Gamma a / Gamma a) = 1
rw₅ : r ^ a * (1 / r) ^ a * 1 = 1
rw₆ : r ^ a * (1 / r) ^ a = 1
rw₇ : r ^ a * (HPow.hPow (α := ℝ) 1 a / r ^ a) = 1
rw₈ : r ^ a * (1 / r ^ a) = 1
rw₉ : r ^ a / r ^ a = 1
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      r ^ a / Gamma a * (a_1 ^ (a - 1) * rexp (-(r * a_1))))
    1
have rw₁₀ : Eq (α := ℝ) 1 1
Tactic: rw [integral_const_mul, integral_rpow_mul_exp_neg_mul_Ioi ha hr, div_mul_eq_mul_div,
      ← mul_assoc, mul_div_assoc, div_self (Gamma_pos_of_pos ha).ne', mul_one,
      div_rpow zero_le_one hr.le, one_rpow, mul_one_div, div_self (rpow_pos_of_pos hr _).ne']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
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)))
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ici 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
have hf : ∀ᵐ (x : ℝ), Membership.mem (γ := Set ℝ) (Ici 0) x → 0 x ≤ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
Tactic: rw [EventuallyLE, ae_restrict_iff' measurableSet_Ici]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
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)))
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) (Measure.restrict volume (Ici 0))
have hfm : gammaPDFReal a r =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ici 0))] fun (x : ℝ) ↦
  r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
Tactic: apply (measurable_gammaPDFReal a r).aestronglyMeasurable.congr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
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))
have hfm : ∀ (x : ℝ) (hx : 0 ≤ x), gammaPDFReal a r x = (fun (x : ℝ) ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) x
Tactic: refine (ae_restrict_iff' measurableSet_Ici).mpr <| ae_of_all _ fun x (hx : 0 ≤ x) ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
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))
⊢ gammaPDFReal a r x = (fun (x : ℝ) ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) x
have 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))
Tactic: simp_rw [gammaPDFReal, eq_true_intro hx, ite_true]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
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))
⊢ gammaPDFReal a r x = (fun (x : ℝ) ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) x
have 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))
Tactic: simp_rw [gammaPDFReal, eq_true_intro hx, ite_true]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (hypothesis)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
⊢ (↑(cdf (gammaMeasure a r)) : ℝ → ℝ) x =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic x)) fun (x : ℝ) ↦ gammaPDFReal a r x
have this : IsProbabilityMeasure (gammaMeasure a r)
Tactic: have : IsProbabilityMeasure (gammaMeasure a r) := isProbabilityMeasure_gammaMeasure ha hr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ (↑(cdf (gammaMeasure a r)) : ℝ → ℝ) x =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic x)) fun (x : ℝ) ↦ gammaPDFReal a r x
have 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
Tactic: rw [cdf_eq_real, gammaMeasure, measureReal_def, withDensity_apply _ measurableSet_Iic]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
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
have refine_1 : 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Iic x))] gammaPDFReal a r
Tactic: refine (integral_eq_lintegral_of_nonneg_ae ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
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
⊢ (∫⁻ (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
have refine_2 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gammaPDFReal a r) (Measure.restrict volume (Iic x))
Tactic: refine (integral_eq_lintegral_of_nonneg_ae ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (hypothesis)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
⊢ (↑(cdf (gammaMeasure a r)) : ℝ → ℝ) x = (∫⁻ (x : ℝ) in Iic x, gammaPDF a r x).toReal
have this : IsProbabilityMeasure (gammaMeasure a r)
Tactic: have : IsProbabilityMeasure (gammaMeasure a r) := isProbabilityMeasure_gammaMeasure ha hr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ (↑(cdf (gammaMeasure a r)) : ℝ → ℝ) x = (∫⁻ (x : ℝ) in Iic x, gammaPDF a r x).toReal
have simp : (gammaMeasure a r).real (Iic x) = (∫⁻ (x : ℝ) in Iic x, ENNReal.ofReal (gammaPDFReal a r x)).toReal
Tactic: simp only [gammaPDF, cdf_eq_real]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (hypothesis)
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∞) ((μ : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have this : 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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ Measure.map (⇑L : (a : ℝ) → ℝ) (gaussianReal m v) =
    gaussianReal (∫ (x : ℝ), (L : (a : ℝ) → ℝ) x ∂gaussianReal m v) Var[(⇑L : (a : ℝ) → ℝ); gaussianReal m v].toNNReal
have 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
Tactic: rw [gaussianReal_map_continuousLinearMap]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ 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
have 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
Tactic: simp only [integral_continuousLinearMap_gaussianReal, variance_continuousLinearMap_gaussianReal,
      Real.coe_toNNReal']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ 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
have e_v : (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v =
  (max (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) 0 * (↑v : ℝ)).toNNReal
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v =
    (max (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) 0 * (↑v : ℝ)).toNNReal
have e_v : (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v =
  (max (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) 0).toNNReal * v
Tactic: rw [Real.toNNReal_mul (by positivity), Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v =
    (max (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) 0).toNNReal * v
have e_v : HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2 =
  max (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) 0
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2 =
    max (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) 0
have e_v : 0 ≤ HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2
Tactic: simp only [left_eq_sup]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
μ : Measure ℝ
h : IsGaussian μ
⊢ Measure.map (⇑(ContinuousLinearMap.id ℝ ℝ) : (a : ℝ) → ℝ) μ = gaussianReal (∫ (x : ℝ), id x ∂μ) Var[id; μ].toNNReal
have rw : gaussianReal (∫ (x : ℝ), (ContinuousLinearMap.id ℝ ℝ : (a : ℝ) → ℝ) x ∂μ)
    Var[(⇑(ContinuousLinearMap.id ℝ ℝ) : (a : ℝ) → ℝ); μ].toNNReal =
  gaussianReal (∫ (x : ℝ), id x ∂μ) Var[id; μ].toNNReal
Tactic: rw [h.map_eq_gaussianReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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 μ
have refine : ∀ (L : StrongDual ℝ E),
  Measure.map (⇑L : (a : E) → ℝ) μ =
    gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal
Tactic: refine ⟨fun L ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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
⊢ Measure.map (⇑L : (a : E) → ℝ) μ =
    gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal
have 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
Tactic: rw [(h L).eq_gaussianReal, integral_map, variance_map]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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
⊢ Measure.map (⇑L : (a : E) → ℝ) μ =
    gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal
have hX : AEMeasurable (α := ℝ) (_m := Real.measurableSpace) id (Measure.map (⇑L : (a : E) → ℝ) μ)
Tactic: rw [(h L).eq_gaussianReal, integral_map, variance_map]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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) → ℝ) μ)
⊢ Measure.map (⇑L : (a : E) → ℝ) μ =
    gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal
have hY : AEMeasurable (β := ℝ) (⇑L : (a : E) → ℝ) μ
Tactic: rw [(h L).eq_gaussianReal, integral_map, variance_map]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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) → ℝ) μ
⊢ Measure.map (⇑L : (a : E) → ℝ) μ =
    gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal
have hfm : AEStronglyMeasurable (α := ℝ) (m₀ := Real.measurableSpace) id (Measure.map (⇑L : (a : E) → ℝ) μ)
Tactic: rw [(h L).eq_gaussianReal, integral_map, variance_map]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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 μ
have refine : ∀ (L : E →L[ℝ] ℝ), IsGaussian (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
Tactic: refine isGaussian_of_isGaussian_map fun L ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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[ℝ] ℝ
⊢ IsGaussian (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
have obtain : ∀ (m : ℝ) (v : ℝ≥0) (h : Measure.map (⇑L : (a : E) → ℝ) μ = gaussianReal m v),
  IsGaussian (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
Tactic: obtain ⟨m, v, h⟩ := h L
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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 (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
have rw : IsGaussian (gaussianReal m v)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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) μ)
have 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
Tactic: refine isGaussian_of_map_eq_gaussianReal fun L' ↦ ⟨μ[L' ∘L L], Var[L' ∘L L; μ].toNNReal, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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[ℝ] ℝ
⊢ Measurable (α := F) (β := ℝ) (⇑L' : (a : F) → ℝ)
have funProp : mF ≤ mF
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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
⊢ Measurable (α := F) (β := ℝ) (⇑L' : (a : F) → ℝ)
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (a : F) ↦ (L' : (a : F) → ℝ) a
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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[ℝ] ℝ
⊢ 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
have rw : Measure.map (Function.comp (β := F) (⇑L' : (a : F) → ℝ) (⇑L : (a : E) → F)) μ =
  gaussianReal (∫ (x : E), (L' ∘SL L : (a : E) → ℝ) x ∂μ) Var[(⇑(L' ∘SL L) : (a : E) → ℝ); μ].toNNReal
Tactic: rw [Measure.map_map (by fun_prop) hL, ← ContinuousLinearMap.coe_comp',
    IsGaussian.map_eq_gaussianReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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[ℝ] ℝ
rw :
  Measure.map (Function.comp (β := F) (⇑L' : (a : F) → ℝ) (⇑L : (a : E) → F)) μ =
    gaussianReal (∫ (x : E), (L' ∘SL L : (a : E) → ℝ) x ∂μ) Var[(⇑(L' ∘SL L) : (a : E) → ℝ); μ].toNNReal
⊢ 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
have rw₁ : Measure.map (⇑(L' ∘SL L) : (a : E) → ℝ) μ =
  gaussianReal (∫ (x : E), (L' ∘SL L : (a : E) → ℝ) x ∂μ) Var[(⇑(L' ∘SL L) : (a : E) → ℝ); μ].toNNReal
Tactic: rw [Measure.map_map (by fun_prop) hL, ← ContinuousLinearMap.coe_comp',
    IsGaussian.map_eq_gaussianReal]