-- 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 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 (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

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

Result:
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)

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

Tactic:
simp only [hc, zero_mul, ne_eq, abs_zero, mul_eq_zero]

Result:
case pos
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : c = 0
⊢ Measure.map (fun x => 0) (gaussianReal μ v) = 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| ≠ 0

Tactic:
rwa [ne_eq, abs_eq_zero]

Result:
no goals

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| = 1

Tactic:
rw [abs_inv, inv_mul_cancel₀]

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| ≠ 0

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)

Tactic:
simp only [e, Homeomorph.mulLeft₀, Equiv.toFun_as_coe, Equiv.mulLeft₀_apply, Equiv.invFun_as_coe,
  Equiv.mulLeft₀_symm_apply, Homeomorph.toMeasurableEquiv_coe, Homeomorph.homeomorph_mk_coe_symm,
  Equiv.coe_fn_symm_mk, gaussianPDFReal_inv_mul hc]

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⁻¹| * (|c| * gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s', 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
⊢ Measure.map (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

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 _)

Result:
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 (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

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:
rw [← NNReal.coe_inj]

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, ⋯⟩ = ↑0

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

Tactic:
rw [Measure.map_const]

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

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

Tactic:
exact Measure.map_dirac (measurable_id'.const_mul c) μ

Result:
no goals

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

Tactic:
by_cases hc : c = 0

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

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

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, ⋯⟩ * v ≠ 0

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

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, ⋯⟩ = 0

Proof state:
μ : ℝ
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

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

Result:
no goals