awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v = 0
pos : Measure.rnDeriv (m := Real.measurableSpace) (Measure.dirac μ) ℙ =ᶠ[ae (F := Measure ℝ) ℙ] 0
⊢ ∂gaussianReal μ v/∂ℙ =ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDF μ v

Tactic:
simp only [hv, gaussianReal_zero_var, gaussianPDF_zero_var]

Premises used: ProbabilityTheory.gaussianReal_zero_var, ProbabilityTheory.gaussianPDF_zero_var
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ Measure.rnDeriv (m := Real.measurableSpace) (Measure.dirac μ) ℙ =ᶠ[ae (F := Measure ℝ) ℙ] 0

Tactic:
(Measure.eq_rnDeriv measurable_zero (mutuallySingular_dirac μ volume) ?_).symm

Premises used: MeasureTheory.mutuallySingular_dirac, MeasureTheory.Measure.eq_rnDeriv, MeasureTheory.MeasureSpace.volume, measurable_zero, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v = 0
pos : Measure.dirac μ = HAdd.hAdd (α := Measure ℝ) (Measure.dirac μ) (Measure.withDensity ℙ 0)
⊢ Measure.rnDeriv (m := Real.measurableSpace) (Measure.dirac μ) ℙ =ᶠ[ae (F := Measure ℝ) ℙ] 0

Tactic:
refine (Measure.eq_rnDeriv measurable_zero (mutuallySingular_dirac μ volume) ?_).symm

Premises used: MeasureTheory.mutuallySingular_dirac, MeasureTheory.Measure.eq_rnDeriv, MeasureTheory.MeasureSpace.volume, measurable_zero, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v = 0
pos : Measure.dirac μ = HAdd.hAdd (α := Measure ℝ) (Measure.dirac μ) 0
pos₁ pos₂ : Eq (α := Measure ℝ) (Measure.dirac μ) (Measure.dirac μ)
⊢ Measure.dirac μ = HAdd.hAdd (α := Measure ℝ) (Measure.dirac μ) (Measure.withDensity ℙ 0)

Tactic:
rw [withDensity_zero, add_zero]

Premises used: MeasureTheory.withDensity_zero, add_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
neg : ∂Measure.withDensity ℙ (gaussianPDF μ v)/∂ℙ =ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDF μ v
⊢ ∂gaussianReal μ v/∂ℙ =ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDF μ v

Tactic:
rw [gaussianReal_of_var_ne_zero _ hv]

Premises used: ProbabilityTheory.gaussianReal_of_var_ne_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ ∂Measure.withDensity ℙ (gaussianPDF μ v)/∂ℙ =ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDF μ v

Tactic:
Measure.rnDeriv_withDensity _ (measurable_gaussianPDF μ v)

Premises used: ProbabilityTheory.measurable_gaussianPDF, MeasureTheory.Measure.rnDeriv_withDensity
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ ∂Measure.withDensity ℙ (gaussianPDF μ v)/∂ℙ =ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDF μ v

Tactic:
exact Measure.rnDeriv_withDensity _ (measurable_gaussianPDF μ v)

Premises used: ProbabilityTheory.measurable_gaussianPDF, MeasureTheory.Measure.rnDeriv_withDensity
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : ℝ
v : ℝ≥0
f : ℝ → E
hv : v ≠ 0
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ), f x ∂gaussianReal μ v)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦ gaussianPDFReal μ v x • f x)

Tactic:
simp [gaussianReal, hv,
    integral_withDensity_eq_integral_toReal_smul (measurable_gaussianPDF _ _)
      (ae_of_all _ fun _ ↦ gaussianPDF_lt_top)]

Premises used: ProbabilityTheory.gaussianReal, ProbabilityTheory.measurable_gaussianPDF, integral_withDensity_eq_integral_toReal_smul, MeasureTheory.ae_of_all, ProbabilityTheory.gaussianPDF_lt_top
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ → ℝ
hf : MeasurableEmbedding f
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt f (f' x) x
s : Set ℝ
hs : MeasurableSet s
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))
⊢ (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))

Tactic:
rw [gaussianReal_of_var_ne_zero _ hv, gaussianPDF_def]

Premises used: ProbabilityTheory.gaussianReal_of_var_ne_zero, ProbabilityTheory.gaussianPDF_def
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
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 (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:
hf.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul' hs h_deriv
    (ae_of_all _ (gaussianPDFReal_nonneg _ _)) (integrable_gaussianPDFReal _ _)

Premises used: MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul', MeasureTheory.ae_of_all, ProbabilityTheory.integrable_gaussianPDFReal, ProbabilityTheory.gaussianPDFReal_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
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 (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:
exact hf.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul' hs h_deriv
    (ae_of_all _ (gaussianPDFReal_nonneg _ _)) (integrable_gaussianPDFReal _ _)

Premises used: MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul', MeasureTheory.ae_of_all, ProbabilityTheory.integrable_gaussianPDFReal, ProbabilityTheory.gaussianPDFReal_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ ≃ᵐ ℝ
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt (⇑f : (a : ℝ) → ℝ) (f' x) x
s : Set ℝ
hs : MeasurableSet s
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))
⊢ (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))

Tactic:
rw [gaussianReal_of_var_ne_zero _ hv, gaussianPDF_def]

Premises used: ProbabilityTheory.gaussianReal_of_var_ne_zero, ProbabilityTheory.gaussianPDF_def
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
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 : ℝ) → ℝ)
          (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:
f.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul' hs h_deriv
    (ae_of_all _ (gaussianPDFReal_nonneg _ _)) (integrable_gaussianPDFReal _ _)

Premises used: MeasureTheory.ae_of_all, MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul', ProbabilityTheory.integrable_gaussianPDFReal, ProbabilityTheory.gaussianPDFReal_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
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 : ℝ) → ℝ)
          (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:
exact f.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul' hs h_deriv
    (ae_of_all _ (gaussianPDFReal_nonneg _ _)) (integrable_gaussianPDFReal _ _)

Premises used: MeasureTheory.ae_of_all, MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul', ProbabilityTheory.integrable_gaussianPDFReal, ProbabilityTheory.gaussianPDFReal_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
pos : ∀ (hv : v = 0), Measure.map (fun (x : ℝ) ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v
neg : ∀ (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

Tactic:
by_cases hv : v = 0
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
hv : v = 0
⊢ Measure.map (fun (x : ℝ) ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

Tactic:
simp [hv, gaussianReal_zero_var]

Premises used: ProbabilityTheory.gaussianReal_zero_var
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.addRight y))
⊢ ∀ (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
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
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
neg : Measure.map (⇑e.symm : (a : ℝ) → ℝ) (gaussianReal μ v) = gaussianReal (μ + y) v
⊢ Measure.map (fun (x : ℝ) ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

Tactic:
change (gaussianReal μ v).map e.symm = gaussianReal (μ + y) v

Premises used: ProbabilityTheory.gaussianReal, MeasurableEquiv.symm, HAdd.hAdd, MeasureTheory.Measure.map, DFunLike.coe
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
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
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∞)
⊢ Measure.map (⇑e.symm : (a : ℝ) → ℝ) (gaussianReal μ v) = gaussianReal (μ + y) v

Tactic:
ext s' hs'
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
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'
neg :
  ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        |1| * gaussianPDFReal μ v ((e : (a : ℝ) → ℝ) x)) =
    (gaussianReal (μ + y) v : (a : Set ℝ) → ℝ≥0∞) s'
⊢ Eq (α := ℝ≥0∞) ((Measure.map (⇑e.symm : (a : ℝ) → ℝ) (gaussianReal μ v) : (a : Set ℝ) → ℝ≥0∞) s' : ℝ≥0∞)
    ((gaussianReal (μ + y) v : (a : Set ℝ) → ℝ≥0∞) s' : ℝ≥0∞)

Tactic:
rw [MeasurableEquiv.gaussianReal_map_symm_apply hv e he' hs']

Premises used: MeasurableEquiv.gaussianReal_map_symm_apply
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
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'
neg :
  ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        gaussianPDFReal μ v ((e : (a : ℝ) → ℝ) x)) =
    (gaussianReal (μ + y) v : (a : Set ℝ) → ℝ≥0∞) s'
⊢ ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        |1| * gaussianPDFReal μ v ((e : (a : ℝ) → ℝ) x)) =
    (gaussianReal (μ + y) v : (a : Set ℝ) → ℝ≥0∞) s'

Tactic:
simp only [abs_one, one_mul]

Premises used: abs_one, one_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
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'
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)
⊢ ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        gaussianPDFReal μ v ((e : (a : ℝ) → ℝ) x)) =
    (gaussianReal (μ + y) v : (a : Set ℝ) → ℝ≥0∞) s'

Tactic:
rw [gaussianReal_apply_eq_integral _ hv s']

Premises used: ProbabilityTheory.gaussianReal_apply_eq_integral
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
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)) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        gaussianPDFReal (μ + y) v x)

Tactic:
simp [e, gaussianPDFReal_sub _ y, Homeomorph.addRight, ← sub_eq_add_neg]

Premises used: sub_eq_add_neg, ProbabilityTheory.gaussianPDFReal_sub, Homeomorph.addRight
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
simp_rw : Measure.map (fun (x : ℝ) ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v
⊢ Measure.map (fun (x : ℝ) ↦ y + x) (gaussianReal μ v) = gaussianReal (μ + y) v

Tactic:
simp_rw [add_comm y]

Premises used: add_comm
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
⊢ Measure.map (fun (x : ℝ) ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

Tactic:
gaussianReal_map_add_const y

Premises used: ProbabilityTheory.gaussianReal_map_add_const
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
⊢ Measure.map (fun (x : ℝ) ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

Tactic:
exact gaussianReal_map_add_const y

Premises used: ProbabilityTheory.gaussianReal_map_add_const
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
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)
neg :
  ∀ (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)

Tactic:
by_cases hv : v = 0
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : v = 0
⊢ Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)

Tactic:
simp [hv, mul_zero, gaussianReal_zero_var]

Premises used: ProbabilityTheory.gaussianReal_zero_var, MulZeroClass.mul_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
pos :
  ∀ (hc : c = 0),
    Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) =
      gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)
neg :
  ∀ (hc : ¬c = 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)

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : c = 0
⊢ Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)

Tactic:
simp [hc, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
this : ∀ (x : ℝ), HasDerivAt (fun (x : ℝ) ↦ c⁻¹ * x) (c⁻¹ * 1) x
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : ∀ (x : ℝ), HasDerivAt (fun (x : ℝ) ↦ c⁻¹ * x) c⁻¹ x) (x : ℝ),
    HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
⊢ ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x

Tactic:
rwa [mul_one] at this

Premises used: mul_one
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
suffices : ∀ (x : ℝ), HasDerivAt (fun (x : ℝ) ↦ c⁻¹ * x) (c⁻¹ * 1) x
⊢ ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x

Tactic:
suffices ∀ x, HasDerivAt (fun x => c⁻¹ * x) (c⁻¹ * 1) x by rwa [mul_one] at this
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
⊢ ∀ (x : ℝ), HasDerivAt (fun (x : ℝ) ↦ c⁻¹ * x) (c⁻¹ * 1) x

Tactic:
fun _ ↦ HasDerivAt.const_mul _ (hasDerivAt_id _)

Premises used: hasDerivAt_id, Inv.inv, HasDerivAt.const_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
⊢ ∀ (x : ℝ), HasDerivAt (fun (x : ℝ) ↦ c⁻¹ * x) (c⁻¹ * 1) x

Tactic:
exact fun _ ↦ HasDerivAt.const_mul _ (hasDerivAt_id _)

Premises used: HasDerivAt.const_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
⊢ ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x

Tactic:
have he' : ∀ x, HasDerivAt e ((fun _ ↦ c⁻¹) x) x := by
    suffices ∀ x, HasDerivAt (fun x => c⁻¹ * x) (c⁻¹ * 1) x by rwa [mul_one] at this
    exact fun _ ↦ HasDerivAt.const_mul _ (hasDerivAt_id _)
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
neg :
  Measure.map (⇑e.symm : (a : ℝ) → ℝ) (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)

Tactic:
change (gaussianReal μ v).map e.symm = gaussianReal (c * μ) (.mk (c ^ 2) (sq_nonneg _) * v)

Premises used: HMul.hMul, ProbabilityTheory.gaussianReal, MeasurableEquiv.symm, MeasureTheory.Measure.map, DFunLike.coe
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
neg :
  ∀ (s' : Set ℝ) (hs' : MeasurableSet s'),
    Eq (α := ℝ≥0∞) ((Measure.map (⇑e.symm : (a : ℝ) → ℝ) (gaussianReal μ v) : (a : Set ℝ) → ℝ≥0∞) s' : ℝ≥0∞)
      ((gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) : (a : Set ℝ) → ℝ≥0∞) s' : ℝ≥0∞)
⊢ Measure.map (⇑e.symm : (a : ℝ) → ℝ) (gaussianReal μ v) =
    gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)

Tactic:
ext s' hs'
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
neg :
  ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        |c⁻¹| * gaussianPDFReal μ v ((e : (a : ℝ) → ℝ) x)) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x)
rw : NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v ≠ 0
⊢ Eq (α := ℝ≥0∞) ((Measure.map (⇑e.symm : (a : ℝ) → ℝ) (gaussianReal μ v) : (a : Set ℝ) → ℝ≥0∞) s' : ℝ≥0∞)
    ((gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) : (a : Set ℝ) → ℝ≥0∞) s' : ℝ≥0∞)

Tactic:
rw [MeasurableEquiv.gaussianReal_map_symm_apply hv e he' hs',
    gaussianReal_apply_eq_integral _ _ s']

Premises used: MeasurableEquiv.gaussianReal_map_symm_apply, ProbabilityTheory.gaussianReal_apply_eq_integral
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
simp : ¬NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ = 0
⊢ NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v ≠ 0

Tactic:
simp only [ne_eq, mul_eq_zero, hv, or_false]

Premises used: mul_eq_zero, ne_eq, or_false
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
rw : ¬(↑(NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯) : ℝ) = (↑0 : ℝ)
⊢ ¬NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ = 0

Tactic:
rw [← NNReal.coe_inj]

Premises used: NNReal.coe_inj
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ¬(↑(NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯) : ℝ) = (↑0 : ℝ)

Tactic:
simp [hc]