awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
⊢ ∀ᵐ (ω : E) ∂P,
    Tendsto (fun (n : ℕ) ↦ (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω) atTop
      (𝓝 (ε.mulExpNegMulSq ((g : (a : E) → ℝ) ω)))
have h_lim : ∀ (x : E),
  Tendsto (fun (n : ℕ) ↦ (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x) atTop
    (𝓝 (ε.mulExpNegMulSq ((g : (a : E) → ℝ) x)))
Tactic: apply Eventually.of_forall
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
x : E
⊢ Tendsto (fun (n : ℕ) ↦ (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x) atTop
    (𝓝 (ε.mulExpNegMulSq ((g : (a : E) → ℝ) x)))
have h_lim : Tendsto (fun (x_1 : ℕ) ↦ ((1 + HSMul.hSMul (α := ℝ) (↑x_1 : ℝ)⁻¹ (-(ε • g * g))) ^ x_1 : (a : E) → ℝ) x) atTop
  (𝓝 (rexp (-HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))))
Tactic: apply Tendsto.const_mul (g x)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst_4 : IsFiniteMeasure P'
A : Subalgebra ℝ (E →ᵇ ℝ)
hε : 0 < ε
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
g : E →ᵇ ℝ
hgA : g ∈ A
n : ℕ
⊢ g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n ∈ A
have apply : 1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g)) ∈ A
Tactic: apply Subalgebra.mul_mem A hgA (Subalgebra.pow_mem A _ n)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst_4 : IsFiniteMeasure P'
A : Subalgebra ℝ (E →ᵇ ℝ)
hε : 0 < ε
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
g : E →ᵇ ℝ
hgA : g ∈ A
n : ℕ
⊢ 1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g)) ∈ A
have apply : -(ε • g * g) ∈ A
Tactic: apply Subalgebra.add_mem A (Subalgebra.one_mem A) (Subalgebra.smul_mem A _ n⁻¹)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (hypothesis)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst_4 : IsFiniteMeasure P'
A : Subalgebra ℝ (E →ᵇ ℝ)
hε : 0 < ε
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
g : E →ᵇ ℝ
hgA : g ∈ A
⊢ Eq (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
    (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')
have one_add_inv_mul_mem : ∀ (n : ℕ), g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n ∈ A
Tactic: have one_add_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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst_4 : IsFiniteMeasure P'
A : Subalgebra ℝ (E →ᵇ ℝ)
hε : 0 < ε
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
g : E →ᵇ ℝ
hgA : g ∈ A
one_add_inv_mul_mem : ∀ (n : ℕ), g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n ∈ A
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦ ∫ (x : E), (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x ∂P) atTop
    (𝓝 (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P'))
have rw : Tendsto (β := ℝ)
  (fun (n : ℕ) ↦ ∫ (x : E), (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x ∂P') atTop
  (𝓝 (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P'))
Tactic: rw [funext fun n => heq _ (one_add_inv_mul_mem n)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (hypothesis)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst_4 : IsFiniteMeasure P'
A : Subalgebra ℝ (E →ᵇ ℝ)
hε : 0 < ε
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
g : E →ᵇ ℝ
hgA : g ∈ A
one_add_inv_mul_mem : ∀ (n : ℕ), g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n ∈ A
⊢ Eq (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
    (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')
have limP : Tendsto (β := ℝ)
  (fun (n : ℕ) ↦ ∫ (x : E), (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x ∂P) atTop
  (𝓝 (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P'))
Tactic: have limP : Tendsto (fun n : ℕ => ∫ x, (g * (1 + (n : ℝ)⁻¹ • -(ε • g * g)) ^ n) x ∂P) atTop
      (𝓝 (∫ x, mulExpNegMulSq ε (g x) ∂P')) := by
    rw [funext fun n => heq _ (one_add_inv_mul_mem n)]
    exact tendsto_integral_mul_one_add_inv_smul_sq_pow g hε
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
K : Set E
hK : MeasurableSet K
hε : 0 < ε
hKP : (P : (a : Set E) → ℝ≥0∞) Kᶜ < (↑ε.toNNReal : ℝ≥0∞)
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)| <
    √ε
have apply : P.real Kᶜ * (√ε)⁻¹ < √ε
Tactic: apply lt_of_le_of_lt (norm_integral_sub_setIntegral_le
    (Eventually.of_forall (fun _ => abs_mulExpNegMulSq_le hε)) hK
    (integrable_mulExpNegMulSq_comp f hε))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
K : Set E
hK : MeasurableSet K
hε : 0 < ε
hKP : (P : (a : Set E) → ℝ≥0∞) Kᶜ < (↑ε.toNNReal : ℝ≥0∞)
⊢ P.real Kᶜ * (√ε)⁻¹ < √ε
have rw : P.real Kᶜ < ε
Tactic: rw [mul_inv_lt_iff₀ (sqrt_pos_of_pos hε), mul_self_sqrt (le_of_lt hε)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
K : Set E
hK : IsCompact K
hKmeas : MeasurableSet K
f g : C(E, ℝ)
δ : ℝ
hε : 0 < ε
hfg : ∀ x ∈ K, |HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)| < δ
⊢ |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)| ≤
    δ * ENNReal.toReal ((P : (a : Set E) → ℝ≥0∞) K)
have rw : Norm.norm (E := ℝ)
    (∫ (a : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) a) - ε.mulExpNegMulSq ((f : (a : E) → ℝ) a) ∂P) ≤
  δ * ENNReal.toReal ((P : (a : Set E) → ℝ≥0∞) K)
Tactic: rw [← (integral_sub (integrable_mulExpNegMulSq_comp_restrict_of_isCompact hK hKmeas g)
      (integrable_mulExpNegMulSq_comp_restrict_of_isCompact hK hKmeas f)), ← norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have pos : ∀ (hPP' : P = 0 ∧ P' = 0),
  |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
Tactic: by_cases hPP' : P = 0 ∧ P' = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
pos :
  ∀ (hPP' : P = 0 ∧ P' = 0),
    |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
          (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
      6 * √ε
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have neg : ∀ (hPP' : ¬(P = 0 ∧ P' = 0)),
  |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
Tactic: by_cases hPP' : P = 0 ∧ P' = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
⊢ 0 < const
have rw : ∀ (hPP' : ¬P = 0 ∨ ¬P' = 0),
  let const := max (P.real Set.univ) (P'.real Set.univ);
  0 < const
Tactic: rw [not_and_or] at hPP'
Cleared hypotheses: hPP', const
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬P = 0 ∨ ¬P' = 0
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
⊢ 0 < const
have inl : ∀ (hP0 : ¬P = 0), 0 < const
Tactic: rcases hPP' with hP0 | hP'0
Cleared hypotheses: hPP'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬P = 0 ∨ ¬P' = 0
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
inl : ∀ (hP0 : ¬P = 0), 0 < const
⊢ 0 < const
have inr : ∀ (hP'0 : ¬P' = 0), 0 < const
Tactic: rcases hPP' with hP0 | hP'0
Cleared hypotheses: hPP'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (hypothesis)
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have pos_of_measure : 0 < const
Tactic: have pos_of_measure : 0 < const := by
    rw [not_and_or] at hPP'
    rcases hPP' with hP0 | hP'0
    · exact lt_max_of_lt_left
        (toReal_pos ((Measure.measure_univ_ne_zero).mpr hP0) (by finiteness))
    · exact lt_max_of_lt_right
        (toReal_pos ((Measure.measure_univ_ne_zero).mpr hP'0) (by finiteness))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have neg : ∀ KP ⊆ Set.univ,
  ∀ (hKPco : IsCompact KP) (hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP)
    (hKP : (P : (a : Set E) → ℝ≥0∞) (Set.univ \ KP) < ENNReal.ofReal ε),
    |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
          (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
      6 * √ε
Tactic: obtain ⟨KP, _, hKPco, hKPcl, hKP⟩ := MeasurableSet.exists_isCompact_isClosed_diff_lt
    (MeasurableSet.univ) (measure_ne_top P Set.univ) (ofReal_pos.mpr hε).ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
hKP : (P : (a : Set E) → ℝ≥0∞) (Set.univ \ KP) < ENNReal.ofReal ε
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have neg : ∀ KP' ⊆ Set.univ,
  ∀ (hKP'co : IsCompact KP') (hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP')
    (hKP' : (P' : (a : Set E) → ℝ≥0∞) (Set.univ \ KP') < ENNReal.ofReal ε),
    |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
          (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
      6 * √ε
Tactic: obtain ⟨KP', _, hKP'co, hKP'cl, hKP'⟩ := MeasurableSet.exists_isCompact_isClosed_diff_lt
    (MeasurableSet.univ) (measure_ne_top P' Set.univ) (ofReal_pos.mpr hε).ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (hypothesis)
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
hKP : (P : (a : Set E) → ℝ≥0∞) (Set.univ \ KP) < ENNReal.ofReal ε
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
hKP' : (P' : (a : Set E) → ℝ≥0∞) (Set.univ \ KP') < ENNReal.ofReal ε
K : Set E := KP ∪ KP'
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have hKco : IsCompact (KP ∪ KP')
Tactic: have hKco := IsCompact.union hKPco hKP'co
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (hypothesis)
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
hKP : (P : (a : Set E) → ℝ≥0∞) (Set.univ \ KP) < ENNReal.ofReal ε
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
hKP' : (P' : (a : Set E) → ℝ≥0∞) (Set.univ \ KP') < ENNReal.ofReal ε
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
Tactic: have hKcl := IsClosed.union hKPcl hKP'cl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (hypothesis)
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
hKP : (P : (a : Set E) → ℝ≥0∞) (Set.univ \ KP) < ENNReal.ofReal ε
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
hKP' : (P' : (a : Set E) → ℝ≥0∞) (Set.univ \ KP') < ENNReal.ofReal ε
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have hKP₁ : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
Tactic: simp only [← Set.compl_eq_univ_diff] at hKP hKP'
Cleared hypotheses: hKP, hKP'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (hypothesis)
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
hKP : (P : (a : Set E) → ℝ≥0∞) (Set.univ \ KP) < ENNReal.ofReal ε
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
hKP' : (P' : (a : Set E) → ℝ≥0∞) (Set.univ \ KP') < ENNReal.ofReal ε
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP₁ : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have hKP'₁ : (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε
Tactic: simp only [← Set.compl_eq_univ_diff] at hKP hKP'
Cleared hypotheses: hKP, hKP'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (hypothesis)
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
hKP' : (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
Tactic: have hKPbound : P (KP ∪ KP')ᶜ < ε.toNNReal := lt_of_le_of_lt
        (measure_mono (Set.compl_subset_compl_of_subset (Set.subset_union_left))) hKP