-- Mathlib/Probability/Distributions/Gaussian.lean
/-- The map of a Gaussian distribution by multiplication by a constant is a Gaussian. -/
lemma gaussianReal_map_const_mul (c : ℝ) :
    (gaussianReal μ v).map (c * ·) = gaussianReal (c * μ) (⟨c^2, sq_nonneg _⟩ * v)

Proof state:
case pos
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : c = 0
⊢ Measure.dirac 0 = gaussianReal 0 (⟨0 ^ 2, ⋯⟩ * v)

Tactic:
convert (gaussianReal_zero_var 0).symm

Result:
case h.e'_3.h.e'_2
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : c = 0
⊢ ⟨0 ^ 2, ⋯⟩ * v = 0

Proof state:
case pos
μ : ℝ
v : ℝ≥0
c : ℝ
hv : v = 0
⊢ Measure.map (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

Tactic:
simp only [hv, mul_zero, ne_eq, not_true, gaussianReal_zero_var]

Result:
case pos
μ : ℝ
v : ℝ≥0
c : ℝ
hv : v = 0
⊢ Measure.map (fun x => c * x) (Measure.dirac μ) = Measure.dirac (c * μ)

Proof state:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
this : ∀ (x : ℝ), HasDerivAt (fun x => c⁻¹ * x) (c⁻¹ * 1) x
⊢ ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x

Tactic:
rwa [mul_one] at this

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ¬↑⟨c ^ 2, ⋯⟩ = ↑0

Tactic:
simp [hc]

Result:
no goals

Proof state:
case h.e'_3.h.e'_2
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : c = 0
⊢ ⟨0 ^ 2, ⋯⟩ * v = 0

Tactic:
simp only [ne_eq, zero_pow, mul_eq_zero, hv, or_false, not_false_eq_true, reduceCtorEq,
  NNReal.mk_zero]

Result:
no goals

Proof state:
case neg.h
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal (∫ (x : ℝ) in s', |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x)

Tactic:
congr with x

Result:
case neg.h.e_r.e_f.h
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
⊢ |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x) = gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x

Proof state:
case neg
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x
⊢ Measure.map (⇑e.symm) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

Tactic:
ext s' hs'

Result:
case neg.h
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ (Measure.map (⇑e.symm) (gaussianReal μ v)) s' = (gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)) s'

Proof state:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
this : |c⁻¹| * |c| = 1
⊢ |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x) = gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x

Tactic:
rw [← mul_assoc, this, one_mul]

Result:
no goals

Proof state:
case neg.h
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ (Measure.map (⇑e.symm) (gaussianReal μ v)) s' = (gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)) s'

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

Result:
case neg.h
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal (∫ (x : ℝ) in s', |c⁻¹| * gaussianPDFReal μ v (e x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x)

μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ⟨c ^ 2, ⋯⟩ * v ≠ 0

Proof state:
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ Measure.map (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

Tactic:
by_cases hv : v = 0

Result:
case pos
μ : ℝ
v : ℝ≥0
c : ℝ
hv : v = 0
⊢ Measure.map (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

case neg
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
⊢ Measure.map (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

Proof state:
case neg
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
⊢ Measure.map (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

Tactic:
let e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv

Result:
case neg
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
⊢ Measure.map (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

Proof state:
case pos
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : c = 0
⊢ (gaussianReal μ v) Set.univ • Measure.dirac 0 = gaussianReal 0 (⟨0 ^ 2, ⋯⟩ * v)

Tactic:
simp only [ne_eq, measure_univ, one_smul, mul_eq_zero]

Result:
case pos
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : c = 0
⊢ Measure.dirac 0 = gaussianReal 0 (⟨0 ^ 2, ⋯⟩ * v)

Proof state:
case neg.h.e_r.e_f.h
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
⊢ |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x) = gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x

Tactic:
suffices |c⁻¹| * |c| = 1 by rw [← mul_assoc, this, one_mul]

Result:
case neg.h.e_r.e_f.h
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
⊢ |c⁻¹| * |c| = 1

Proof state:
case neg.h
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal (∫ (x : ℝ) in s', |c⁻¹| * gaussianPDFReal μ v (e x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x)

μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ⟨c ^ 2, ⋯⟩ * v ≠ 0

Tactic:
swap

Result:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ⟨c ^ 2, ⋯⟩ * v ≠ 0

case neg.h
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal (∫ (x : ℝ) in s', |c⁻¹| * gaussianPDFReal μ v (e x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x)

Proof state:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
⊢ ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x

Tactic:
suffices ∀ x, HasDerivAt (fun x => c⁻¹ * x) (c⁻¹ * 1) x by rwa [mul_one] at this

Result:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
⊢ ∀ (x : ℝ), HasDerivAt (fun x => c⁻¹ * x) (c⁻¹ * 1) x