-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean
theorem integral_mulExpNegMulSq_comp_eq {P' : Measure E} [IsFiniteMeasure P']
    {A : Subalgebra ℝ C(E, ℝ)} (hε : 0 < ε)
    (hbound : ∀ g ∈ A, ∃ C, ∀ x y : E, dist (g x) (g y) ≤ C)
    (heq : ∀ g ∈ A, ∫ x, (g : E → ℝ) x ∂P = ∫ x, (g : E → ℝ) x ∂P') {g : C(E, ℝ)} (hgA : g ∈ A) :
    ∫ x, mulExpNegMulSq ε (g x) ∂P = ∫ x, mulExpNegMulSq ε (g x) ∂P'

Proof state:
E : Type u_1
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
P : Measure E
inst✝¹ : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst✝ : IsFiniteMeasure P'
A : Subalgebra ℝ C(E, ℝ)
hε : 0 < ε
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
g : C(E, ℝ)
hgA : g ∈ A
C : ℝ
h : ∀ (x y : E), dist (g x) (g y) ≤ C
one_plus_inv_mul_mem : ∀ (n : ℕ), g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n ∈ A
⊢ Tendsto (fun n => ∫ (x : E), (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) x ∂P) atTop
    (𝓝 (∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'))

Tactic:
rw [funext fun n => heq _ (one_plus_inv_mul_mem n)]

Result:
E : Type u_1
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
P : Measure E
inst✝¹ : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst✝ : IsFiniteMeasure P'
A : Subalgebra ℝ C(E, ℝ)
hε : 0 < ε
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
g : C(E, ℝ)
hgA : g ∈ A
C : ℝ
h : ∀ (x y : E), dist (g x) (g y) ≤ C
one_plus_inv_mul_mem : ∀ (n : ℕ), g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n ∈ A
⊢ Tendsto (fun n => ∫ (x : E), (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) x ∂P') atTop
    (𝓝 (∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'))

Proof state:
E : Type u_1
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
P : Measure E
inst✝¹ : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst✝ : IsFiniteMeasure P'
A : Subalgebra ℝ C(E, ℝ)
hε : 0 < ε
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
g : C(E, ℝ)
hgA : g ∈ A
C : ℝ
h : ∀ (x y : E), dist (g x) (g y) ≤ C
n : ℕ
⊢ -(ε • g * g) ∈ A

Tactic:
exact Subalgebra.neg_mem A (Subalgebra.mul_mem A (Subalgebra.smul_mem A hgA ε) hgA)

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
P : Measure E
inst✝¹ : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst✝ : IsFiniteMeasure P'
A : Subalgebra ℝ C(E, ℝ)
hε : 0 < ε
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
g : C(E, ℝ)
hgA : g ∈ A
C : ℝ
h : ∀ (x y : E), dist (g x) (g y) ≤ C
n : ℕ
⊢ g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n ∈ A

Tactic:
apply Subalgebra.mul_mem A hgA (Subalgebra.pow_mem A _ n)

Result:
E : Type u_1
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
P : Measure E
inst✝¹ : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst✝ : IsFiniteMeasure P'
A : Subalgebra ℝ C(E, ℝ)
hε : 0 < ε
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
g : C(E, ℝ)
hgA : g ∈ A
C : ℝ
h : ∀ (x y : E), dist (g x) (g y) ≤ C
n : ℕ
⊢ 1 + (↑n)⁻¹ • -(ε • g * g) ∈ A

Proof state:
E : Type u_1
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
P : Measure E
inst✝¹ : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst✝ : IsFiniteMeasure P'
A : Subalgebra ℝ C(E, ℝ)
hε : 0 < ε
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
g : C(E, ℝ)
hgA : g ∈ A
C : ℝ
h : ∀ (x y : E), dist (g x) (g y) ≤ C
one_plus_inv_mul_mem : ∀ (n : ℕ), g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n ∈ A
⊢ Tendsto (fun n => ∫ (x : E), (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) x ∂P') atTop
    (𝓝 (∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'))

Tactic:
exact tendsto_integral_mul_one_plus_inv_smul_sq_pow (mkOfBound g C h) hε

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
P : Measure E
inst✝¹ : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst✝ : IsFiniteMeasure P'
A : Subalgebra ℝ C(E, ℝ)
hε : 0 < ε
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
g : C(E, ℝ)
hgA : g ∈ A
⊢ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P = ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'

Tactic:
obtain ⟨C, h⟩ := hbound g hgA

Result:
case intro
E : Type u_1
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
P : Measure E
inst✝¹ : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst✝ : IsFiniteMeasure P'
A : Subalgebra ℝ C(E, ℝ)
hε : 0 < ε
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
g : C(E, ℝ)
hgA : g ∈ A
C : ℝ
h : ∀ (x y : E), dist (g x) (g y) ≤ C
⊢ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P = ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'

Proof state:
case intro
E : Type u_1
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
P : Measure E
inst✝¹ : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst✝ : IsFiniteMeasure P'
A : Subalgebra ℝ C(E, ℝ)
hε : 0 < ε
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
g : C(E, ℝ)
hgA : g ∈ A
C : ℝ
h : ∀ (x y : E), dist (g x) (g y) ≤ C
⊢ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P = ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'

Tactic:
have one_plus_inv_mul_mem (n : ℕ) : g * (1 + (n : ℝ)⁻¹ • -(ε • g * g)) ^ n ∈ A := by
  apply Subalgebra.mul_mem A hgA (Subalgebra.pow_mem A _ n)
  apply Subalgebra.add_mem A (Subalgebra.one_mem A) (Subalgebra.smul_mem A _ n⁻¹)
  exact Subalgebra.neg_mem A (Subalgebra.mul_mem A (Subalgebra.smul_mem A hgA ε) hgA)

Result:
case intro
E : Type u_1
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
P : Measure E
inst✝¹ : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst✝ : IsFiniteMeasure P'
A : Subalgebra ℝ C(E, ℝ)
hε : 0 < ε
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
g : C(E, ℝ)
hgA : g ∈ A
C : ℝ
h : ∀ (x y : E), dist (g x) (g y) ≤ C
one_plus_inv_mul_mem : ∀ (n : ℕ), g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n ∈ A
⊢ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P = ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'

Proof state:
case intro
E : Type u_1
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
P : Measure E
inst✝¹ : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst✝ : IsFiniteMeasure P'
A : Subalgebra ℝ C(E, ℝ)
hε : 0 < ε
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
g : C(E, ℝ)
hgA : g ∈ A
C : ℝ
h : ∀ (x y : E), dist (g x) (g y) ≤ C
one_plus_inv_mul_mem : ∀ (n : ℕ), g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n ∈ A
limP :
  Tendsto (fun n => ∫ (x : E), (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) x ∂P) atTop
    (𝓝 (∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'))
⊢ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P = ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'

Tactic:
exact tendsto_nhds_unique
  (tendsto_integral_mul_one_plus_inv_smul_sq_pow (mkOfBound g C h) hε) limP

Result:
no goals