OAI/Analysis/FourierLLogL/Thermal/Levels.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Asymptotic scales for the dyadic bound

  1. def OAI.FourierLLogL.Dyadic.Thermal.H line 12
  2. def OAI.FourierLLogL.Dyadic.Thermal.plateErr line 14
  3. def OAI.FourierLLogL.Dyadic.Thermal.mainIx line 16

    Source documentation

    Index depth i denotes b=2^{-i}; b₀=h^{-16}.

    def mainIx (j : ℕ) := 16*ell j
  4. def OAI.FourierLLogL.Dyadic.Thermal.testIx line 17
  5. def OAI.FourierLLogL.Dyadic.Thermal.beta line 18
  6. def OAI.FourierLLogL.Dyadic.Thermal.kappa line 20

    Source documentation

    Linear growth is enough for the normalization coding sizes

    def kappa (j : ℕ) (A0 : ℝ) (i : ℕ) := A0 * height j / H j * (1+i)

    Mentions: OAI.FourierLLogL.Dyadic.Thermal.H

  7. def OAI.FourierLLogL.Dyadic.Thermal.eps line 21
  8. lemma OAI.FourierLLogL.Dyadic.Thermal.H_ge line 23
  9. lemma OAI.FourierLLogL.Dyadic.Thermal.H_pos line 24
  10. lemma OAI.FourierLLogL.Dyadic.Thermal.d_pos line 25
  11. lemma OAI.FourierLLogL.Dyadic.Thermal.beta_pos line 26
  12. lemma OAI.FourierLLogL.Dyadic.Thermal.beta_le line 27
  13. lemma OAI.FourierLLogL.Dyadic.Thermal.eps_pos line 28
  14. lemma OAI.FourierLLogL.Dyadic.Thermal.kappa_pos line 29
  15. lemma OAI.FourierLLogL.Dyadic.Thermal.beta_log line 32
  16. lemma OAI.FourierLLogL.Dyadic.Thermal.h_large line 39
  17. lemma OAI.FourierLLogL.Dyadic.Thermal.hpow_index line 44
  18. lemma OAI.FourierLLogL.Dyadic.Thermal.hpoly line 48
  19. lemma OAI.FourierLLogL.Dyadic.Thermal.hpoly_mix line 53
  20. lemma OAI.FourierLLogL.Dyadic.Thermal.bottom_level line 59
  21. lemma OAI.FourierLLogL.Dyadic.Thermal.main_bounds line 62
  22. lemma OAI.FourierLLogL.Dyadic.Thermal.sigma_small line 79
  23. lemma OAI.FourierLLogL.Dyadic.Thermal.Tk_bounds line 97
  24. lemma OAI.FourierLLogL.Dyadic.Thermal.kappa_scales line 105
  25. lemma OAI.FourierLLogL.Dyadic.Thermal.stiff_budget line 143