awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
hε : 0 < ε
x y : ℝ
h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ (↑1 : ℝ≥0∞) * edist x y
rwa :
  ∀ (h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ 1 * edist x y),
    dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
have rwa₁ : ∀ (h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ edist x y),
  dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
Tactic: rwa [ENNReal.coe_one, one_mul, ← (toReal_le_toReal (edist_ne_top _ _) (edist_ne_top _ _))] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
hε : 0 < ε
x y : ℝ
h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ (↑1 : ℝ≥0∞) * edist x y
rwa :
  ∀ (h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ 1 * edist x y),
    dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
rwa₁ :
  ∀ (h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ edist x y),
    dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
have rwa₂ : ∀ (h : (edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y)).toReal ≤ (edist x y).toReal),
  dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
Tactic: rwa [ENNReal.coe_one, one_mul, ← (toReal_le_toReal (edist_ne_top _ _) (edist_ne_top _ _))] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (hypothesis)
Goal:
x : ℝ
⊢ Tendsto (fun (ε : ℝ) ↦ ε.mulExpNegMulSq x) (𝓝 0) (𝓝 x)
have this : x = (fun (ε : ℝ) ↦ ε.mulExpNegMulSq x) 0
Tactic: have : x = (fun ε : ℝ => mulExpNegMulSq ε x) 0 := by
    simp only [mulExpNegMulSq, zero_mul, neg_zero, exp_zero, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
x : ℝ
this : x = (fun (ε : ℝ) ↦ ε.mulExpNegMulSq x) 0
⊢ Tendsto (fun (ε : ℝ) ↦ ε.mulExpNegMulSq x) (𝓝 0) (𝓝 x)
have nth_rw : Tendsto (β := ℝ) (fun (ε : ℝ) ↦ ε.mulExpNegMulSq x) (𝓝 0) (𝓝 ((fun (ε : ℝ) ↦ ε.mulExpNegMulSq x) 0))
Tactic: nth_rw 2 [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
E : Type u_1
inst : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ |(ε.mulExpNegMulSq ∘ (⇑g : (a : E) → ℝ)) x| ≤ ‖g‖
have simp : HMul.hMul (α := ℝ) (|(g : (a : E) → ℝ) x| : ℝ)
    (rexp (-HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))) ≤
  ‖g‖
Tactic: simp only [Function.comp_apply, mulExpNegMulSq, abs_mul, abs_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
E : Type u_1
inst : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ HMul.hMul (α := ℝ) (|(g : (a : E) → ℝ) x| : ℝ)
      (rexp (-HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))) ≤
    ‖g‖
have apply : rexp (-HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ)) ≤ 1
Tactic: apply le_trans (mul_le_of_le_one_right (abs_nonneg (g x)) _) (g.norm_coe_le_norm x)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq (goal)
Goal:
ε : ℝ
E : Type u_1
inst : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ rexp (-HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ)) ≤ 1
have rw : 0 ≤ ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ)
Tactic: rw [exp_le_one_iff, Left.neg_nonpos_iff, mul_assoc]
-- 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, ℝ)
hε : 0 < ε
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ε.mulExpNegMulSq ((f : (a : E) → ℝ) x)) P
have apply : ∀ (x y : E),
  dist
      (ContinuousMap.toFun
        { toFun := fun (x : E) ↦ ε.mulExpNegMulSq ((f : (a : E) → ℝ) x), continuous_toFun := sorry : C(E, ℝ) } x)
      (ContinuousMap.toFun
        { toFun := fun (x : E) ↦ ε.mulExpNegMulSq ((f : (a : E) → ℝ) x), continuous_toFun := sorry : C(E, ℝ) } y) ≤
    2 * (√ε)⁻¹
Tactic: apply integrable P ⟨⟨fun x => mulExpNegMulSq ε (f x), by fun_prop⟩, ⟨2 * (√ε)⁻¹, _⟩⟩
-- 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 →ᵇ ℝ
⊢ Tendsto (β := ℝ) (fun (ε : ℝ) ↦ ∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P) (𝓝[>] 0)
    (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂P))
have a : ∀ (x : ℕ → ℝ),
  Tendsto x atTop (𝓝[>] 0) →
    Tendsto (β := ℝ) ((fun (ε : ℝ) ↦ ∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P) ∘ x) atTop
      (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂P))
Tactic: apply tendsto_of_seq_tendsto
-- 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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
⊢ Tendsto (β := ℝ) ((fun (ε : ℝ) ↦ ∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P) ∘ u) atTop
    (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂P))
have a : ∀ (N : ℕ) (hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)),
  Tendsto (β := ℝ) ((fun (ε : ℝ) ↦ ∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P) ∘ u) atTop
    (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂P))
Tactic: obtain ⟨N, hupos⟩ := eventually_atTop.mp (tendsto_nhdsWithin_iff.mp hu).2
-- 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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)
⊢ Tendsto (β := ℝ) ((fun (ε : ℝ) ↦ ∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P) ∘ u) atTop
    (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂P))
have h_meas : ∀ᶠ (n : ℕ) in atTop, AEStronglyMeasurable (β := ℝ) (fun (ω : E) ↦ (u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)) P
Tactic: apply tendsto_integral_filter_of_norm_le_const ?h_meas ?h_bound ?h_lim
-- 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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)
h_meas : ∀ᶠ (n : ℕ) in atTop, AEStronglyMeasurable (β := ℝ) (fun (ω : E) ↦ (u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)) P
⊢ Tendsto (β := ℝ) ((fun (ε : ℝ) ↦ ∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P) ∘ u) atTop
    (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂P))
have h_bound : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ C
Tactic: apply tendsto_integral_filter_of_norm_le_const ?h_meas ?h_bound ?h_lim
-- 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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)
h_meas : ∀ᶠ (n : ℕ) in atTop, AEStronglyMeasurable (β := ℝ) (fun (ω : E) ↦ (u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)) P
h_bound : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ C
⊢ Tendsto (β := ℝ) ((fun (ε : ℝ) ↦ ∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P) ∘ u) atTop
    (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂P))
have h_lim : ∀ᵐ (ω : E) ∂P,
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)) atTop (𝓝 ((g : (a : E) → ℝ) ω) : Filter ℝ)
Tactic: apply tendsto_integral_filter_of_norm_le_const ?h_meas ?h_bound ?h_lim
-- 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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)
⊢ ∃ (C : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ C
have h : ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ ‖g‖
Tactic: use norm g
-- 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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ ‖g‖
have h : ∃ (a : ℕ), ∀ b ≥ a, ∀ᵐ (ω : E) ∂P, ‖(u b).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ ‖g‖
Tactic: rw [eventually_atTop]
-- 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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)
⊢ ∃ (a : ℕ), ∀ b ≥ a, ∀ᵐ (ω : E) ∂P, ‖(u b).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ ‖g‖
have h : ∀ b ≥ N, ∀ᵐ (ω : E) ∂P, ‖(u b).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ ‖g‖
Tactic: use 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
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
⊢ 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 h_meas : ∀ᶠ (n : ℕ) in atTop,
  AEStronglyMeasurable (β := ℝ) (⇑(g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n) : (a : E) → ℝ) P
Tactic: apply tendsto_integral_filter_of_norm_le_const ?h_meas ?h_bound ?h_lim
-- 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 < ε
h_meas :
  ∀ᶠ (n : ℕ) in atTop,
    AEStronglyMeasurable (β := ℝ) (⇑(g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n) : (a : E) → ℝ) P
⊢ 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 h_bound : ∃ (C : ℝ),
  ∀ᶠ (n : ℕ) in atTop,
    ∀ᵐ (ω : E) ∂P,
      Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω : ℝ) ≤ C
Tactic: apply tendsto_integral_filter_of_norm_le_const ?h_meas ?h_bound ?h_lim
-- 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 < ε
h_meas :
  ∀ᶠ (n : ℕ) in atTop,
    AEStronglyMeasurable (β := ℝ) (⇑(g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n) : (a : E) → ℝ) P
h_bound :
  ∃ (C : ℝ),
    ∀ᶠ (n : ℕ) in atTop,
      ∀ᵐ (ω : E) ∂P,
        Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω : ℝ) ≤ C
⊢ 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 h_lim : ∀ᵐ (ω : E) ∂P,
  Tendsto (fun (n : ℕ) ↦ (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω) atTop
    (𝓝 (ε.mulExpNegMulSq ((g : (a : E) → ℝ) ω)))
Tactic: apply tendsto_integral_filter_of_norm_le_const ?h_meas ?h_bound ?h_lim
-- 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 < ε
⊢ ∀ᶠ (n : ℕ) in atTop,
    AEStronglyMeasurable (β := ℝ) (⇑(g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n) : (a : E) → ℝ) P
have h_meas : ∀ (x : ℕ),
  AEStronglyMeasurable (β := ℝ) (⇑(g * (1 + HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹ (-(ε • g * g))) ^ x) : (a : E) → ℝ) P
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 < ε
⊢ ∃ (C : ℝ),
    ∀ᶠ (n : ℕ) in atTop,
      ∀ᵐ (ω : E) ∂P,
        Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω : ℝ) ≤ C
have h_bound : ∀ (N : ℕ) (hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)),
  ∃ (C : ℝ),
    ∀ᶠ (n : ℕ) in atTop,
      ∀ᵐ (ω : E) ∂P,
        Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω : ℝ) ≤ C
Tactic: obtain ⟨N, hgN⟩ := exists_nat_gt (ε * (norm g * norm g))
-- 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 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)
⊢ ∃ (C : ℝ),
    ∀ᶠ (n : ℕ) in atTop,
      ∀ᵐ (ω : E) ∂P,
        Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω : ℝ) ≤ C
have h : ∀ᶠ (n : ℕ) in atTop,
  ∀ᵐ (ω : E) ∂P,
    Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω : ℝ) ≤ ‖g‖
Tactic: use norm g
-- 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 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ᵐ (ω : E) ∂P,
      Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω : ℝ) ≤ ‖g‖
have h : ∃ (a : ℕ),
  ∀ b ≥ a,
    ∀ᵐ (ω : E) ∂P,
      Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑b : ℝ)⁻¹ (-(ε • g * g))) ^ b : (a : E) → ℝ) ω : ℝ) ≤ ‖g‖
Tactic: rw [eventually_atTop]
-- 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 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)
⊢ ∃ (a : ℕ),
    ∀ b ≥ a,
      ∀ᵐ (ω : E) ∂P,
        Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑b : ℝ)⁻¹ (-(ε • g * g))) ^ b : (a : E) → ℝ) ω : ℝ) ≤ ‖g‖
have h : ∀ b ≥ N,
  ∀ᵐ (ω : E) ∂P,
    Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑b : ℝ)⁻¹ (-(ε • g * g))) ^ b : (a : E) → ℝ) ω : ℝ) ≤ ‖g‖
Tactic: use 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
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)
n : ℕ
hn : n ≥ N
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)
have apply : 0 ≤ ε * (‖g‖ * ‖g‖)
Tactic: apply lt_of_lt_of_le (lt_of_le_of_lt _ hgN) (Nat.cast_le.mpr hn)
-- 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
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)
n : ℕ
hn : n ≥ N
⊢ ∀ᵐ (ω : E) ∂P,
    Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω : ℝ) ≤ ‖g‖
have hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: have hnpos : 0 < (n : ℝ) := by
      apply lt_of_lt_of_le (lt_of_le_of_lt _ hgN) (Nat.cast_le.mpr hn)
      exact (mul_nonneg (le_of_lt hε) (mul_self_nonneg (norm g)))
-- 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 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)
n : ℕ
hn : n ≥ N
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ ∀ᵐ (ω : E) ∂P,
    Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω : ℝ) ≤ ‖g‖
have h : ∀ (x : E), Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x : ℝ) ≤ ‖g‖
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 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)
n : ℕ
hn : n ≥ N
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : E
⊢ Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x : ℝ) ≤ ‖g‖
have h : HMul.hMul (α := ℝ) (|(g : (a : E) → ℝ) x| : ℝ)
    (|1 +
          -((↑n : ℝ)⁻¹ *
              HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))| ^
      n) ≤
  ‖g‖
Tactic: simp only [smul_neg, BoundedContinuousFunction.coe_mul, Pi.mul_apply, pow_apply,
      BoundedContinuousFunction.coe_add, BoundedContinuousFunction.coe_one, coe_neg,
      BoundedContinuousFunction.coe_smul, smul_eq_mul, Pi.add_apply, Pi.one_apply, Pi.neg_apply,
      norm_mul, norm_eq_abs, norm_pow]
-- 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 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)
n : ℕ
hn : n ≥ N
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : E
⊢ HMul.hMul (α := ℝ) (|(g : (a : E) → ℝ) x| : ℝ)
      (|1 +
            -((↑n : ℝ)⁻¹ *
                HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))| ^
        n) ≤
    ‖g‖
have h : |1 + -((↑n : ℝ)⁻¹ * HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))| ^
    n ≤
  1
Tactic: refine (mul_le_mul_of_nonneg_right (norm_coe_le_norm g x) (pow_nonneg (abs_nonneg _) n)).trans
      <| mul_le_of_le_one_right (norm_nonneg _) ?_
-- 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 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)
n : ℕ
hn : n ≥ N
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : E
⊢ |1 + -((↑n : ℝ)⁻¹ * HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))| ^
      n ≤
    1
have h : |1 + -((↑n : ℝ)⁻¹ * HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))| ≤ 1
Tactic: apply pow_le_one₀ (abs_nonneg _)
-- 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 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)
n : ℕ
hn : n ≥ N
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : E
⊢ |1 + -((↑n : ℝ)⁻¹ * HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))| ≤
    1
have h : -1 ≤ 1 + -(ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) / (↑n : ℝ)) ∧
  1 + -(ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) / (↑n : ℝ)) ≤ 1
Tactic: rw [mul_assoc, inv_mul_eq_div, abs_le]
-- 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 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)
n : ℕ
hn : n ≥ N
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : E
⊢ -1 ≤ 1 + -(ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) / (↑n : ℝ)) ∧
    1 + -(ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) / (↑n : ℝ)) ≤ 1
have h : -1 ≤ 1 + -(ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) / (↑n : ℝ))
Tactic: refine ⟨?_, (add_le_iff_nonpos_right 1).mpr (Left.neg_nonpos_iff.mpr
      (div_nonneg (mul_nonneg (le_of_lt hε) (mul_self_nonneg (g x))) (le_of_lt hnpos)))⟩
-- 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 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)
n : ℕ
hn : n ≥ N
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : E
⊢ LE.le (α := ℝ) (-1) 0
have linarith : LT.lt (α := ℝ) 0 (-1) → -1 + HSub.hSub (α := ℝ) 0 (-1) = 0
Tactic: linarith
-- 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 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)
n : ℕ
hn : n ≥ N
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : E
⊢ -1 ≤ 1 + -(ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) / (↑n : ℝ))
have apply : ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) ≤ (↑n : ℝ)
Tactic: apply le_trans (by linarith) (sub_nonneg_of_le ((div_le_one hnpos).mpr _))
-- 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 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)
n : ℕ
hn : n ≥ N
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : E
⊢ ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) ≤ (↑n : ℝ)
have apply : ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) ≤ ε * (‖g‖ * ‖g‖)
Tactic: apply le_trans (le_trans _ (le_of_lt hgN)) (Nat.cast_le.mpr hn)
-- 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 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)
n : ℕ
hn : n ≥ N
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : E
⊢ ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) ≤ ε * (‖g‖ * ‖g‖)
have apply : HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) ≤ ‖g‖ * ‖g‖
Tactic: apply mul_le_mul (le_refl ε) _ (mul_self_nonneg (g x)) (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
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < (↑N : ℝ)
n : ℕ
hn : n ≥ N
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : E
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) ≤ ‖g‖ * ‖g‖
have rw : |(g : (a : E) → ℝ) x| ≤ ‖g‖
Tactic: rw [← abs_le_iff_mul_self_le, abs_norm]