-- Mathlib/Probability/Distributions/Gaussian.lean
/-- The map of a Gaussian distribution by addition of a constant is a Gaussian. -/
lemma gaussianReal_map_add_const (y : ℝ) :
    (gaussianReal μ v).map (· + y) = gaussianReal (μ + y) v

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

Tactic:
exact Measure.map_dirac (measurable_id'.add_const _) _

Result:
no goals

Proof state:
case neg.h
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal μ v (e x)) = (gaussianReal (μ + y) v) s'

Tactic:
rw [gaussianReal_apply_eq_integral _ hv s']

Result:
case neg.h
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal μ v (e x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal (μ + y) v x)

Proof state:
case neg.h
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal (∫ (x : ℝ) in s', |1| * gaussianPDFReal μ v (e x)) = (gaussianReal (μ + y) v) s'

Tactic:
simp only [abs_neg, abs_one, MeasurableEquiv.coe_mk, Equiv.coe_fn_mk, one_mul, ne_eq]

Result:
case neg.h
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal μ v (e x)) = (gaussianReal (μ + y) v) s'

Proof state:
case neg
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv
⊢ Measure.map (fun x => x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

Tactic:
have he' : ∀ x, HasDerivAt e ((fun _ ↦ 1) x) x := fun _ ↦ (hasDerivAt_id _).sub_const y

Result:
case neg
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x
⊢ Measure.map (fun x => x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

Proof state:
case neg
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x
⊢ Measure.map (⇑e.symm) (gaussianReal μ v) = gaussianReal (μ + y) v

Tactic:
ext s' hs'

Result:
case neg.h
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ (Measure.map (⇑e.symm) (gaussianReal μ v)) s' = (gaussianReal (μ + y) v) s'

Proof state:
case neg.h
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal μ v (e x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal (μ + y) v x)

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

Result:
no goals

Proof state:
case pos
μ : ℝ
v : ℝ≥0
y : ℝ
hv : v = 0
⊢ Measure.map (fun x => x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

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

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

Proof state:
μ : ℝ
v : ℝ≥0
y : ℝ
⊢ Measure.map (fun x => x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

Tactic:
by_cases hv : v = 0

Result:
case pos
μ : ℝ
v : ℝ≥0
y : ℝ
hv : v = 0
⊢ Measure.map (fun x => x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

case neg
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
⊢ Measure.map (fun x => x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

Proof state:
case neg
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x
⊢ Measure.map (fun x => x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

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

Result:
case neg
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x
⊢ Measure.map (⇑e.symm) (gaussianReal μ v) = gaussianReal (μ + y) v

Proof state:
case neg
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
⊢ Measure.map (fun x => x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

Tactic:
let e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv

Result:
case neg
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv
⊢ Measure.map (fun x => x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

Proof state:
case neg.h
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ (Measure.map (⇑e.symm) (gaussianReal μ v)) s' = (gaussianReal (μ + y) v) s'

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

Result:
case neg.h
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal (∫ (x : ℝ) in s', |1| * gaussianPDFReal μ v (e x)) = (gaussianReal (μ + y) v) s'