OAI/Analysis/Mahler/MassLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.massBelow line 11
2. lemma OAI.Mahler.massBelow_mono line 15
3. lemma OAI.Mahler.massBelow_one line 22
4. theorem OAI.Mahler.massIntegral_lower_of_sublevels line 28

   Source documentation

   Lower bounds on a sublevel sequence tending to one imply the mass bound, even if the final integral is infinite. The sublevel bounds are explicit hypotheses.

   theorem massIntegral_lower_of_sublevels (U : Set (ComplexEuclidean n))
       (f : Fin N → ComplexEuclidean n → ℂ) (m : ℕ) {R : ℕ → ℝ}
       (hR : Tendsto R atTop (𝓝 1)) (hR1 : ∀ k, R k ≤ 1)
       (hbound : ∀ k, ENNReal.ofReal ((R k)^n * (Real.pi * (m : ℝ))^n) ≤ massBelow U f (R k)) :
       ENNReal.ofReal ((Real.pi * (m : ℝ))^n) ≤ massIntegral U f := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.massBelow, OAI.Mahler.massIntegral