awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
h_lim :
  ∀ᵐ (ω : E) ∂P,
    Tendsto (fun (n : ℕ) ↦ (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω) atTop
      (𝓝 (ε.mulExpNegMulSq ((g : (a : E) → ℝ) ω)))
⊢ 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:
apply tendsto_integral_filter_of_norm_le_const ?h_meas ?h_bound ?h_lim
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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 :
  ∀ (x : ℕ),
    AEStronglyMeasurable (β := ℝ) (⇑(g * (1 + HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹ (-(ε • g * g))) ^ x) : (a : E) → ℝ) P
⊢ ∀ᶠ (n : ℕ) in atTop,
    AEStronglyMeasurable (β := ℝ) (⇑(g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n) : (a : E) → ℝ) P

Tactic:
apply Eventually.of_forall

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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 : ℕ),
    AEStronglyMeasurable (β := ℝ) (⇑(g * (1 + HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹ (-(ε • g * g))) ^ x) : (a : E) → ℝ) P

Tactic:
fun n => StronglyMeasurable.aestronglyMeasurable (Continuous.stronglyMeasurable
        (Continuous.mul g.continuous ((1 + ((n : ℝ)⁻¹ • -(ε • g * g))) ^ n).continuous))

Premises used: HMul.hMul, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, BoundedContinuousFunction.continuous, Continuous.stronglyMeasurable, Nat.cast, Continuous.mul, Inv.inv, HPow.hPow, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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 : ℕ),
    AEStronglyMeasurable (β := ℝ) (⇑(g * (1 + HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹ (-(ε • g * g))) ^ x) : (a : E) → ℝ) P

Tactic:
exact fun n => StronglyMeasurable.aestronglyMeasurable (Continuous.stronglyMeasurable
        (Continuous.mul g.continuous ((1 + ((n : ℝ)⁻¹ • -(ε • g * g))) ^ n).continuous))
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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_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
⊢ ∃ (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))

Premises used: Norm.norm, HMul.hMul, exists_nat_gt
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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 : ℝ)
h :
  ∀ᶠ (n : ℕ) in atTop,
    ∀ᵐ (ω : E) ∂P,
      Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω : ℝ) ≤ ‖g‖
⊢ ∃ (C : ℝ),
    ∀ᶠ (n : ℕ) in atTop,
      ∀ᵐ (ω : E) ∂P,
        Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω : ℝ) ≤ C

Tactic:
use norm g

Premises used: Norm.norm
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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 : ℝ)
h :
  ∃ (a : ℕ),
    ∀ b ≥ a,
      ∀ᵐ (ω : E) ∂P,
        Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑b : ℝ)⁻¹ (-(ε • g * g))) ^ b : (a : E) → ℝ) ω : ℝ) ≤ ‖g‖
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ᵐ (ω : E) ∂P,
      Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω : ℝ) ≤ ‖g‖

Tactic:
rw [eventually_atTop]

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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 : ℝ)
h :
  ∀ b ≥ N,
    ∀ᵐ (ω : E) ∂P,
      Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑b : ℝ)⁻¹ (-(ε • g * g))) ^ b : (a : E) → ℝ) ω : ℝ) ≤ ‖g‖
⊢ ∃ (a : ℕ),
    ∀ b ≥ a,
      ∀ᵐ (ω : E) ∂P,
        Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑b : ℝ)⁻¹ (-(ε • g * g))) ^ b : (a : E) → ℝ) ω : ℝ) ≤ ‖g‖

Tactic:
use N
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
apply : 0 ≤ ε * (‖g‖ * ‖g‖)
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
apply lt_of_lt_of_le (lt_of_le_of_lt _ hgN) (Nat.cast_le.mpr hn)

Premises used: Iff.mpr, lt_of_le_of_lt, Nat.cast_le, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
⊢ 0 ≤ ε * (‖g‖ * ‖g‖)

Tactic:
(mul_nonneg (le_of_lt hε) (mul_self_nonneg (norm g)))

Premises used: mul_self_nonneg, Norm.norm, mul_nonneg, le_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
⊢ 0 ≤ ε * (‖g‖ * ‖g‖)

Tactic:
exact (mul_nonneg (le_of_lt hε) (mul_self_nonneg (norm g)))

Premises used: mul_self_nonneg, Norm.norm, mul_nonneg, le_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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 : ℝ)

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)))
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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 : ℝ)
h :
  ∀ (x : E),
    Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x : ℝ) ≤ ‖g‖
⊢ ∀ᵐ (ω : E) ∂P,
    Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω : ℝ) ≤ ‖g‖

Tactic:
apply Eventually.of_forall

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
h :
  HMul.hMul (α := ℝ) (|(g : (a : E) → ℝ) x| : ℝ)
      (|1 +
            -((↑n : ℝ)⁻¹ *
                HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))| ^
        n) ≤
    ‖g‖
⊢ Norm.norm (E := ℝ) ((g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x : ℝ) ≤ ‖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]

Premises used: BoundedContinuousFunction.coe_one, Pi.mul_apply, BoundedContinuousFunction.coe_neg, norm_pow, BoundedContinuousFunction.coe_mul, BoundedContinuousFunction.coe_smul, Pi.one_apply, BoundedContinuousFunction.pow_apply, smul_neg, norm_mul, BoundedContinuousFunction.coe_add, Pi.add_apply, smul_eq_mul, Pi.neg_apply, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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‖

Tactic:
(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 _) ?_

Premises used: pow_nonneg, mul_le_of_le_one_right, mul_le_mul_of_nonneg_right, BoundedContinuousFunction.norm_coe_le_norm, LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
h :
  |1 + -((↑n : ℝ)⁻¹ * HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))| ^
      n ≤
    1
⊢ HMul.hMul (α := ℝ) (|(g : (a : E) → ℝ) x| : ℝ)
      (|1 +
            -((↑n : ℝ)⁻¹ *
                HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))| ^
        n) ≤
    ‖g‖

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 _) ?_

Premises used: pow_nonneg, mul_le_of_le_one_right, mul_le_mul_of_nonneg_right, BoundedContinuousFunction.norm_coe_le_norm, LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
h :
  |1 + -((↑n : ℝ)⁻¹ * HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))| ≤
    1
⊢ |1 + -((↑n : ℝ)⁻¹ * HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))| ^
      n ≤
    1

Tactic:
apply pow_le_one₀ (abs_nonneg _)

Premises used: pow_le_one₀
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
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
⊢ |1 + -((↑n : ℝ)⁻¹ * HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))| ≤
    1

Tactic:
rw [mul_assoc, inv_mul_eq_div, abs_le]

Premises used: abs_le, mul_assoc, inv_mul_eq_div
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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

Tactic:
⟨?_, (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)))⟩

Premises used: mul_self_nonneg, Iff.mpr, mul_nonneg, add_le_iff_nonpos_right, le_of_lt, Left.neg_nonpos_iff, And.intro, div_nonneg, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
h : -1 ≤ 1 + -(ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) / (↑n : ℝ))
⊢ -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:
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)))⟩
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
linarith : LT.lt (α := ℝ) 0 (-1) → -1 + HSub.hSub (α := ℝ) 0 (-1) = 0
⊢ LE.le (α := ℝ) (-1) 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
apply : ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) ≤ (↑n : ℝ)
⊢ -1 ≤ 1 + -(ε * 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 _))

Premises used: Iff.mpr, sub_nonneg_of_le, div_le_one, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
apply : ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) ≤ ε * (‖g‖ * ‖g‖)
⊢ ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) ≤ (↑n : ℝ)

Tactic:
apply le_trans (le_trans _ (le_of_lt hgN)) (Nat.cast_le.mpr hn)

Premises used: Iff.mpr, le_of_lt, Nat.cast_le, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
apply : HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) ≤ ‖g‖ * ‖g‖
⊢ ε * 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ε)

Premises used: mul_self_nonneg, le_refl, le_of_lt, mul_le_mul, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
rw : |(g : (a : E) → ℝ) x| ≤ ‖g‖
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ) ≤ ‖g‖ * ‖g‖

Tactic:
rw [← abs_le_iff_mul_self_le, abs_norm]

Premises used: abs_norm, abs_le_iff_mul_self_le
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
⊢ |(g : (a : E) → ℝ) x| ≤ ‖g‖

Tactic:
norm_coe_le_norm g x

Premises used: BoundedContinuousFunction.norm_coe_le_norm
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
⊢ |(g : (a : E) → ℝ) x| ≤ ‖g‖

Tactic:
exact norm_coe_le_norm g x

Premises used: BoundedContinuousFunction.norm_coe_le_norm
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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_lim :
  ∀ (x : E),
    Tendsto (fun (n : ℕ) ↦ (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x) atTop
      (𝓝 (ε.mulExpNegMulSq ((g : (a : E) → ℝ) x)))
⊢ ∀ᵐ (ω : E) ∂P,
    Tendsto (fun (n : ℕ) ↦ (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) ω) atTop
      (𝓝 (ε.mulExpNegMulSq ((g : (a : E) → ℝ) ω)))

Tactic:
apply Eventually.of_forall

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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
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 : ℝ))))
⊢ Tendsto (fun (n : ℕ) ↦ (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x) atTop
    (𝓝 (ε.mulExpNegMulSq ((g : (a : E) → ℝ) x)))

Tactic:
apply Tendsto.const_mul (g x)

Premises used: Filter.Tendsto.const_mul, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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 (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:
simpa [mul_assoc, inv_mul_eq_div, ← neg_div] using
      tendsto_one_add_div_pow_exp (-(ε * (g x * g x)))

Premises used: neg_div, HMul.hMul, mul_assoc, inv_mul_eq_div, DFunLike.coe, Neg.neg, Real.tendsto_one_add_div_pow_exp
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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 : ℕ
apply : 1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g)) ∈ A
⊢ g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n ∈ A

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

Premises used: Subalgebra.mul_mem, Subalgebra.pow_mem
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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 : ℕ
apply : -(ε • g * g) ∈ A
⊢ 1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g)) ∈ A

Tactic:
apply Subalgebra.add_mem A (Subalgebra.one_mem A) (Subalgebra.smul_mem A _ n⁻¹)

Premises used: Subalgebra.add_mem, Nat.cast, Subalgebra.smul_mem, Inv.inv, Subalgebra.one_mem
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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 * g) ∈ A

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

Premises used: Subalgebra.mul_mem, Set.Mem, setOf, Subalgebra.neg_mem, Subalgebra.smul_mem
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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 * g) ∈ A

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

Premises used: Subalgebra.mul_mem, Subalgebra.neg_mem, Subalgebra.smul_mem
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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

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)