awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (hypothesis)
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
h : ∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x) = 1
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦ gaussianPDFReal μ v x) 1
have h₁ : ENNReal.ofReal (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦ gaussianPDFReal μ v x) =
  ENNReal.ofReal 1
Tactic: rw [← ofReal_integral_eq_lintegral_ofReal (integrable_gaussianPDFReal _ _)
    (ae_of_all _ (gaussianPDFReal_nonneg _ _)), ← ENNReal.ofReal_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
x y : ℝ
⊢ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - y - μ) 2 / (2 * (↑v : ℝ))) =
    (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - (μ + y)) 2 / (2 * (↑v : ℝ)))
have rw : (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - y - μ) 2 / (2 * (↑v : ℝ))) =
  (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - y - μ) 2 / (2 * (↑v : ℝ)))
Tactic: rw [sub_add_eq_sub_sub_swap]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
x y : ℝ
⊢ gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ - y) v x
have rw : gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ + -y) v x
Tactic: rw [sub_eq_add_neg, ← gaussianPDFReal_sub, sub_eq_add_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
x y : ℝ
rw : gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ + -y) v x
⊢ gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ - y) v x
have rw₁ : gaussianPDFReal μ v (x + y) = gaussianPDFReal μ v (x - -y)
Tactic: rw [sub_eq_add_neg, ← gaussianPDFReal_sub, sub_eq_add_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
x y : ℝ
rw : gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ + -y) v x
rw₁ : gaussianPDFReal μ v (x + y) = gaussianPDFReal μ v (x - -y)
⊢ gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ - y) v x
have rw₂ : gaussianPDFReal μ v (x + y) = gaussianPDFReal μ v (x + - -y)
Tactic: rw [sub_eq_add_neg, ← gaussianPDFReal_sub, sub_eq_add_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
x y : ℝ
rw : gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ + -y) v x
rw₁ : gaussianPDFReal μ v (x + y) = gaussianPDFReal μ v (x - -y)
rw₂ : gaussianPDFReal μ v (x + y) = gaussianPDFReal μ v (x + - -y)
⊢ gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ - y) v x
have rw₃ : gaussianPDFReal μ v (x + y) = gaussianPDFReal μ v (x + y)
Tactic: rw [sub_eq_add_neg, ← gaussianPDFReal_sub, sub_eq_add_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ gaussianPDFReal μ v (c⁻¹ * x) = |c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x
have simp : (√(↑v : ℝ))⁻¹ * (√(2 * π))⁻¹ * rexp (-HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ))) =
  |c| *
    ((√(2 * π * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))⁻¹ *
      rexp (-HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ)))))
Tactic: simp only [gaussianPDFReal.eq_1, NNReal.zero_le_coe,
    Real.sqrt_mul', mul_inv_rev, NNReal.coe_mul, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√(↑v : ℝ))⁻¹ * (√(2 * π))⁻¹ * rexp (-HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ))) =
    |c| *
      ((√(2 * π * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))⁻¹ *
        rexp (-HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ)))))
have rw : (√(↑v : ℝ))⁻¹ * (√(2 * π))⁻¹ * rexp (-HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ))) =
  |c| * (√(2 * π * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))⁻¹ *
    rexp (-HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))
Tactic: rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√(↑v : ℝ))⁻¹ * (√(2 * π))⁻¹ * rexp (-HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ))) =
    |c| * (√(2 * π * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))⁻¹ *
      rexp (-HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))
have refine_1 : (√(↑v : ℝ))⁻¹ * (√(2 * π))⁻¹ = |c| * (√(2 * π * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))⁻¹
Tactic: refine congr_arg₂ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
refine_1 : (√(↑v : ℝ))⁻¹ * (√(2 * π))⁻¹ = |c| * (√(2 * π * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))⁻¹
⊢ (√(↑v : ℝ))⁻¹ * (√(2 * π))⁻¹ * rexp (-HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ))) =
    |c| * (√(2 * π * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))⁻¹ *
      rexp (-HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))
have refine_2 : rexp (-HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ))) =
  rexp (-HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))
Tactic: refine congr_arg₂ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√(↑v : ℝ))⁻¹ * (√(2 * π))⁻¹ = |c| * (√(2 * π * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))⁻¹
have refine_1 : √(HPow.hPow (β := ℕ) c 2) / √(↑v : ℝ) = |c| / √(↑v : ℝ)
Tactic: simp (disch := positivity) only [Real.sqrt_mul, mul_inv_rev, field]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ √(HPow.hPow (β := ℕ) c 2) / √(↑v : ℝ) = |c| / √(↑v : ℝ)
have refine_1 : |c| / √(↑v : ℝ) = |c| / √(↑v : ℝ)
Tactic: rw [Real.sqrt_sq_eq_abs]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ rexp (-HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ))) =
    rexp (-HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))
have refine_2 : -HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ)) =
  -HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
| gaussianPDFReal μ v (c * x)
have rw : |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) sorry * v) x
Tactic: rw [← inv_inv c, gaussianPDFReal_inv_mul (inv_ne_zero hc)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ gaussianPDFReal μ v (c * x) = |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2)⁻¹ ⋯ * v) x
have conv_lhs : |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) sorry * v) x =
  |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2)⁻¹ sorry * v) x
Tactic: conv_lhs => rw [← inv_inv c, gaussianPDFReal_inv_mul (inv_ne_zero hc)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
⊢ gaussianPDF μ 0 = 0
have h : ∀ (x : ℝ), gaussianPDF μ 0 x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
x : ℝ
⊢ (gaussianPDF μ v x).toReal = gaussianPDFReal μ v x
have rw : (ENNReal.ofReal (gaussianPDFReal μ v x)).toReal = gaussianPDFReal μ v x
Tactic: rw [gaussianPDF, ENNReal.toReal_ofReal (gaussianPDFReal_nonneg μ v x)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
x : ℝ
rw : (ENNReal.ofReal (gaussianPDFReal μ v x)).toReal = gaussianPDFReal μ v x
⊢ (gaussianPDF μ v x).toReal = gaussianPDFReal μ v x
have rw₁ : gaussianPDFReal μ v x = gaussianPDFReal μ v x
Tactic: rw [gaussianPDF, ENNReal.toReal_ofReal (gaussianPDFReal_nonneg μ v x)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
x : ℝ
⊢ 0 < gaussianPDF μ v x
have rw : 0 < gaussianPDFReal μ v x
Tactic: rw [gaussianPDF, ENNReal.ofReal_pos]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ Function.support (gaussianPDF μ v) = Set.univ
have h : ∀ (x : ℝ), x ∈ Function.support (gaussianPDF μ v) ↔ Membership.mem (γ := Set ℝ) Set.univ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
x : ℝ
⊢ x ∈ Function.support (gaussianPDF μ v) ↔ Membership.mem (γ := Set ℝ) Set.univ x
have h : x ∈ Function.support (gaussianPDF μ v)
Tactic: simp only [Set.mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
⊢ Eq (α := ℝ≥0∞) ((gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have pos : ∀ (h : v = 0), Eq (α := ℝ≥0∞) ((gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: by_cases h : v = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
pos : ∀ (h : v = 0), Eq (α := ℝ≥0∞) ((gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have neg : ∀ (h : ¬v = 0), Eq (α := ℝ≥0∞) ((gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: by_cases h : v = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
⊢ NoAtoms (gaussianReal μ v)
have rw : NoAtoms (m0 := Real.measurableSpace) (Measure.withDensity ℙ (gaussianPDF μ v))
Tactic: rw [gaussianReal_of_var_ne_zero _ h]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ (gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) s = ∫⁻ (x : ℝ) in s, gaussianPDF μ v x
have rw : (Measure.withDensity ℙ (gaussianPDF μ v) : (a : Set ℝ) → ℝ≥0∞) s = ∫⁻ (x : ℝ) in s, gaussianPDF μ v x
Tactic: rw [gaussianReal_of_var_ne_zero _ hv, withDensity_apply' _ s]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
rw : (Measure.withDensity ℙ (gaussianPDF μ v) : (a : Set ℝ) → ℝ≥0∞) s = ∫⁻ (x : ℝ) in s, gaussianPDF μ v x
⊢ (gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) s = ∫⁻ (x : ℝ) in s, gaussianPDF μ v x
have rw₁ : ∫⁻ (a : ℝ) in s, gaussianPDF μ v a = ∫⁻ (x : ℝ) in s, gaussianPDF μ v x
Tactic: rw [gaussianReal_of_var_ne_zero _ hv, withDensity_apply' _ s]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ (gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) s =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s) fun (x : ℝ) ↦ gaussianPDFReal μ v x)
have rw : ∫⁻ (x : ℝ) in s, gaussianPDF μ v x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (gaussianPDFReal μ v x)
Tactic: rw [gaussianReal_apply _ hv s, ofReal_integral_eq_lintegral_ofReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
rw : ∫⁻ (x : ℝ) in s, gaussianPDF μ v x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (gaussianPDFReal μ v x)
⊢ (gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) s =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s) fun (x : ℝ) ↦ gaussianPDFReal μ v x)
have hfi : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (gaussianPDFReal μ v) (Measure.restrict ℙ s)
Tactic: rw [gaussianReal_apply _ hv s, ofReal_integral_eq_lintegral_ofReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
rw : ∫⁻ (x : ℝ) in s, gaussianPDF μ v x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (gaussianPDFReal μ v x)
hfi : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (gaussianPDFReal μ v) (Measure.restrict ℙ s)
⊢ (gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) s =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s) fun (x : ℝ) ↦ gaussianPDFReal μ v x)
have f_nn : 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict ℙ s)] gaussianPDFReal μ v
Tactic: rw [gaussianReal_apply _ hv s, ofReal_integral_eq_lintegral_ofReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ gaussianReal μ v ≪ ℙ
have rw : Measure.withDensity ℙ (gaussianPDF μ v) ≪ ℙ
Tactic: rw [gaussianReal_of_var_ne_zero _ hv]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ℙ ≪ gaussianReal μ v
have rw : ℙ ≪ Measure.withDensity ℙ (gaussianPDF μ v)
Tactic: rw [gaussianReal_of_var_ne_zero _ hv]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ℙ ≪ Measure.withDensity ℙ (gaussianPDF μ v)
have refine_1 : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) (gaussianPDF μ v) ℙ
Tactic: refine withDensity_absolutelyContinuous' ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
refine_1 : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) (gaussianPDF μ v) ℙ
⊢ ℙ ≪ Measure.withDensity ℙ (gaussianPDF μ v)
have refine_2 : ∀ᵐ (x : ℝ), gaussianPDF μ v x ≠ 0
Tactic: refine withDensity_absolutelyContinuous' ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
⊢ ∂gaussianReal μ v/∂ℙ =ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDF μ v
have pos : ∀ (hv : v = 0), ∂gaussianReal μ v/∂ℙ =ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDF μ v
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
pos : ∀ (hv : v = 0), ∂gaussianReal μ v/∂ℙ =ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDF μ v
⊢ ∂gaussianReal μ v/∂ℙ =ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDF μ v
have neg : ∀ (hv : ¬v = 0), ∂gaussianReal μ v/∂ℙ =ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDF μ v
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ ∂gaussianReal μ v/∂ℙ =ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDF μ v
have pos : Measure.rnDeriv (m := Real.measurableSpace) (Measure.dirac μ) ℙ =ᶠ[ae (F := Measure ℝ) ℙ] 0
Tactic: simp only [hv, gaussianReal_zero_var, gaussianPDF_zero_var]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ Measure.rnDeriv (m := Real.measurableSpace) (Measure.dirac μ) ℙ =ᶠ[ae (F := Measure ℝ) ℙ] 0
have pos : Measure.dirac μ = HAdd.hAdd (α := Measure ℝ) (Measure.dirac μ) (Measure.withDensity ℙ 0)
Tactic: refine (Measure.eq_rnDeriv measurable_zero (mutuallySingular_dirac μ volume) ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ Measure.dirac μ = HAdd.hAdd (α := Measure ℝ) (Measure.dirac μ) (Measure.withDensity ℙ 0)
have pos : Measure.dirac μ = HAdd.hAdd (α := Measure ℝ) (Measure.dirac μ) 0
Tactic: rw [withDensity_zero, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v = 0
pos : Measure.dirac μ = HAdd.hAdd (α := Measure ℝ) (Measure.dirac μ) 0
⊢ Measure.dirac μ = HAdd.hAdd (α := Measure ℝ) (Measure.dirac μ) (Measure.withDensity ℙ 0)
have pos₁ : Eq (α := Measure ℝ) (Measure.dirac μ) (Measure.dirac μ)
Tactic: rw [withDensity_zero, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ ∂gaussianReal μ v/∂ℙ =ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDF μ v
have neg : ∂Measure.withDensity ℙ (gaussianPDF μ v)/∂ℙ =ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDF μ v
Tactic: rw [gaussianReal_of_var_ne_zero _ hv]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ → ℝ
hf : MeasurableEmbedding f
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt f (f' x) x
s : Set ℝ
hs : MeasurableSet s
⊢ (Measure.comap f (gaussianReal μ v) : (a : Set ℝ) → ℝ≥0∞) s =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s) fun (x : ℝ) ↦
        |f' x| * gaussianPDFReal μ v (f x))
have rw : (Measure.comap f (Measure.withDensity ℙ fun (x : ℝ) ↦ ENNReal.ofReal (gaussianPDFReal μ v x)) : (a : Set ℝ) → ℝ≥0∞) s =
  ENNReal.ofReal
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s) fun (x : ℝ) ↦
      |f' x| * gaussianPDFReal μ v (f x))
Tactic: rw [gaussianReal_of_var_ne_zero _ hv, gaussianPDF_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ ≃ᵐ ℝ
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt (⇑f : (a : ℝ) → ℝ) (f' x) x
s : Set ℝ
hs : MeasurableSet s
⊢ (Measure.map (⇑f.symm : (a : ℝ) → ℝ) (gaussianReal μ v) : (a : Set ℝ) → ℝ≥0∞) s =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s) fun (x : ℝ) ↦
        |f' x| * gaussianPDFReal μ v ((f : (a : ℝ) → ℝ) x))
have rw : (Measure.map (α := ℝ) (⇑f.symm : (a : ℝ) → ℝ)
        (Measure.withDensity ℙ fun (x : ℝ) ↦ ENNReal.ofReal (gaussianPDFReal μ v x)) :
      (a : Set ℝ) → ℝ≥0∞)
    s =
  ENNReal.ofReal
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s) fun (x : ℝ) ↦
      |f' x| * gaussianPDFReal μ v ((f : (a : ℝ) → ℝ) x))
Tactic: rw [gaussianReal_of_var_ne_zero _ hv, gaussianPDF_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
⊢ Measure.map (fun (x : ℝ) ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v
have pos : ∀ (hv : v = 0), Measure.map (fun (x : ℝ) ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
pos : ∀ (hv : v = 0), Measure.map (fun (x : ℝ) ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v
⊢ Measure.map (fun (x : ℝ) ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v
have neg : ∀ (hv : ¬v = 0), Measure.map (fun (x : ℝ) ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (hypothesis)
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.addRight y))
⊢ Measure.map (fun (x : ℝ) ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v
have he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ (1 : ℝ)) x) x
Tactic: have he' : ∀ x, HasDerivAt e ((fun _ ↦ 1) x) x := fun _ ↦ (hasDerivAt_id _).sub_const y
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.addRight y))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ (1 : ℝ)) x) x
⊢ Measure.map (fun (x : ℝ) ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v
have neg : Measure.map (⇑e.symm : (a : ℝ) → ℝ) (gaussianReal μ v) = gaussianReal (μ + y) v
Tactic: change (gaussianReal μ v).map e.symm = gaussianReal (μ + y) v
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.addRight y))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ (1 : ℝ)) x) x
⊢ Measure.map (⇑e.symm : (a : ℝ) → ℝ) (gaussianReal μ v) = gaussianReal (μ + y) v
have neg : ∀ (s' : Set ℝ) (hs' : MeasurableSet s'),
  Eq (α := ℝ≥0∞) ((Measure.map (⇑e.symm : (a : ℝ) → ℝ) (gaussianReal μ v) : (a : Set ℝ) → ℝ≥0∞) s' : ℝ≥0∞)
    ((gaussianReal (μ + y) v : (a : Set ℝ) → ℝ≥0∞) s' : ℝ≥0∞)
Tactic: ext s' hs'
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.addRight y))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ (1 : ℝ)) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ Eq (α := ℝ≥0∞) ((Measure.map (⇑e.symm : (a : ℝ) → ℝ) (gaussianReal μ v) : (a : Set ℝ) → ℝ≥0∞) s' : ℝ≥0∞)
    ((gaussianReal (μ + y) v : (a : Set ℝ) → ℝ≥0∞) s' : ℝ≥0∞)
have neg : ENNReal.ofReal
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
      |1| * gaussianPDFReal μ v ((e : (a : ℝ) → ℝ) x)) =
  (gaussianReal (μ + y) v : (a : Set ℝ) → ℝ≥0∞) s'
Tactic: rw [MeasurableEquiv.gaussianReal_map_symm_apply hv e he' hs']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.addRight y))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ (1 : ℝ)) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        |1| * gaussianPDFReal μ v ((e : (a : ℝ) → ℝ) x)) =
    (gaussianReal (μ + y) v : (a : Set ℝ) → ℝ≥0∞) s'
have neg : ENNReal.ofReal
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
      gaussianPDFReal μ v ((e : (a : ℝ) → ℝ) x)) =
  (gaussianReal (μ + y) v : (a : Set ℝ) → ℝ≥0∞) s'
Tactic: simp only [abs_one, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.addRight y))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ (1 : ℝ)) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        gaussianPDFReal μ v ((e : (a : ℝ) → ℝ) x)) =
    (gaussianReal (μ + y) v : (a : Set ℝ) → ℝ≥0∞) s'
have neg : ENNReal.ofReal
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
      gaussianPDFReal μ v ((e : (a : ℝ) → ℝ) x)) =
  ENNReal.ofReal
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦ gaussianPDFReal (μ + y) v x)
Tactic: rw [gaussianReal_apply_eq_integral _ hv s']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
⊢ Measure.map (fun (x : ℝ) ↦ y + x) (gaussianReal μ v) = gaussianReal (μ + y) v
have simp_rw : Measure.map (fun (x : ℝ) ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v
Tactic: simp_rw [add_comm y]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)
have pos : ∀ (hv : v = 0),
  Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v)
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
pos :
  ∀ (hv : v = 0),
    Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) =
      gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)
⊢ Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)
have neg : ∀ (hv : ¬v = 0),
  Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v)
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
⊢ Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)
have pos : ∀ (hc : c = 0),
  Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v)
Tactic: by_cases hc : c = 0