awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
Tactic: have hKP'bound : P' (KP ∪ KP')ᶜ < ε.toNNReal := lt_of_le_of_lt
        (measure_mono (Set.compl_subset_compl_of_subset (Set.subset_union_right))) hKP'
-- 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
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 ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have neg : ∀ (g' : C(E, ℝ)) (hg'A : g' ∈ Subalgebra.map (toContinuousMapₐ ℝ) A)
  (hg'approx :
    ∀ x ∈ KP ∪ KP',
      ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹),
  |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
Tactic: obtain ⟨g', hg'A, hg'approx⟩ :=
      ContinuousMap.exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints
      hA f hKco (Left.mul_pos (sqrt_pos_of_pos hε) (inv_pos_of_pos pos_of_measure))
-- 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 ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'A : g' ∈ Subalgebra.map (toContinuousMapₐ ℝ) A
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have hg'A₁ : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
Tactic: simp only [Subalgebra.mem_map] at hg'A
Cleared hypotheses: hg'A
-- 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 ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have hgA : g ∈ A
Tactic: have hgA : g ∈ A := hg'A.choose_spec.1
-- 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
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 ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
hgA : g ∈ A
⊢ ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
have rw : ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
Tactic: rw [← coe_toContinuousMapₐ ℝ g, hg'A.choose_spec.2]
-- 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 ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
hgA : g ∈ A
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have hgapprox : ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
Tactic: have hgapprox : ∀ x ∈ K, ‖g x - f x‖ < √ε * const⁻¹ := by
    rw [← coe_toContinuousMapₐ ℝ g, hg'A.choose_spec.2]
    exact hg'approx
-- 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 ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have line1 : |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
      (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)| <
  √ε
Tactic: have line1 : |∫ x, mulExpNegMulSq ε (f x) ∂P
      - ∫ x in K, mulExpNegMulSq ε (f x) ∂P| < √ε :=
    abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt
      f (IsClosed.measurableSet hKcl) hε hKPbound
-- 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
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 ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
line1 :
  |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)| <
    √ε
⊢ |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)| <
    √ε
have rw : |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
      (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)| <
  √ε
Tactic: rw [abs_sub_comm]
-- 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 ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
line1 :
  |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)| <
    √ε
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have line3 : |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
      (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)| <
  √ε
Tactic: have line3 : |∫ x in K, mulExpNegMulSq ε (g x) ∂P
      - ∫ x, mulExpNegMulSq ε (g x) ∂P| < √ε := by
    rw [abs_sub_comm]
    exact (abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt
      g (IsClosed.measurableSet hKcl) hε hKPbound)
-- 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 ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
line1 :
  |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)| <
    √ε
line3 :
  |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)| <
    √ε
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε
have line5 : |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')
      (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')| <
  √ε
Tactic: have line5 : |∫ x, mulExpNegMulSq ε (g x) ∂P'
      - ∫ x in K, mulExpNegMulSq ε (g x) ∂P'| < √ε :=
    (abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt
      g (IsClosed.measurableSet hKcl) hε hKP'bound)
-- 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
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 ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
line1 :
  |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)| <
    √ε
line3 :
  |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)| <
    √ε
line5 :
  |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')
        (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')| <
    √ε
⊢ |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| <
    √ε
have rw : |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')
      (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| <
  √ε
Tactic: rw [abs_sub_comm]