OAI/Geometry/Convex/GeneralMahler/Rapid.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Polynomial growth and rapid layer decay with polynomial loss in the Gaussian variables. Fubini and moment estimates.

  1. def OAI.GeneralMahler.rapid line 13
  2. def OAI.GeneralMahler.mixed line 15

    Source documentation

    First variable rapid (the tail layer), second moderate (Gaussian).

    def mixed (f:X → Y → E) := ∀ n:ℕ, ∃ (C : ℝ) (m : ℕ), 0≤C ∧ ∀ x y,
…
  3. theorem OAI.GeneralMahler.poly_prod_bound line 18
  4. lemma OAI.GeneralMahler.mixed.poly line 32
  5. lemma OAI.GeneralMahler.mixed.mono line 40
  6. lemma OAI.GeneralMahler.mixed.add line 46
  7. lemma OAI.GeneralMahler.mixed.neg line 56
  8. lemma OAI.GeneralMahler.mixed.sub line 57
  9. lemma OAI.GeneralMahler.mixed.product line 60
  10. lemma OAI.GeneralMahler.mixed.of_cutoff line 76

    Source comment

    Polynomial cutoff in layer
    lemma of_cutoff (hf : PolyBound f.uncurry)
    {d : Y → ℝ} (hd : PolyBound d) (h : ∀ x y, d y < ‖x‖ → f x y = 0) :
    mixed f := by
…

    Mentions: OAI.GeneralMahler.PolyBound, OAI.GeneralMahler.mixed

  11. lemma OAI.GeneralMahler.mixed.of_rapid line 98
  12. lemma OAI.GeneralMahler.envelope_inv_int line 108
  13. lemma OAI.GeneralMahler.mixed_integrable_left line 115
  14. lemma OAI.GeneralMahler.poly_integral_left line 122
  15. lemma OAI.GeneralMahler.mixed_integrable line 142