OAI/Analysis/LipschitzHilbert/Estimates/ExponentialThreshold.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Select the moment order explicitly to absorb a positive global prefactor into the prescribed exponential exceptional-area budget.

  1. theorem OAI.LipschitzHilbert.quarter_ceil_bound line 13
  2. theorem OAI.LipschitzHilbert.prefactor_quarter_ceil_bound line 21
  3. theorem OAI.LipschitzHilbert.prefactor_quarter_successor_bound line 35

    Source documentation

    The extra successor guarantees a positive moment order and retains the requested exponential bound.

    theorem prefactor_quarter_successor_bound (M x : ℝ) (hM : 0 < M) :
    M * (1/4:ℝ)^(⌈(x+Real.log M) / Real.log 4⌉₊+1) ≤ Real.exp (-x) := by
…
  4. theorem OAI.LipschitzHilbert.exponential_moment_order_le line 44
  5. theorem OAI.LipschitzHilbert.polynomial_prefactor_log_le line 60