PowerApproximation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform exponential approximation for the shrinking tail of a simplex.

lemma OAI.TotientAsymptotic.log_one_sub_quadratic line 13

theorem OAI.TotientAsymptotic.simplex_power_approximation line 33

Source documentation

If n*q approaches a bounded nonnegative quantity, the simplex power approaches its exponential, even when that quantity varies with the phase.

theorem simplex_power_approximation {ι : Type*} {l : Filter ι}
    (n : ι → ℕ) (q b : ι → ℝ) (K : ℝ) (_hK : 0 ≤ K)
    (hn : Tendsto n l atTop)
    (hq : ∀ᶠ x in l, 0 ≤ q x)
    (hb : ∀ᶠ x in l, 0 ≤ b x ∧ b x ≤ K)
    (herr : Tendsto (fun x => (n x : ℝ)*q x-b x) l (nhds 0)) :
    Tendsto (fun x => (max (1-q x) 0)^(n x)-Real.exp (-b x)) l (nhds 0) := by
…