OAI/Analysis/FourierLLogL/Thermal/Tilted.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FourierLLogL.Dyadic.Thermal.prob_translate line 16
2. def OAI.FourierLLogL.Dyadic.Thermal.dome line 23

   Source documentation

   label cutoff by reference radius

   def dome (p : Node) (M : ℕ) (s : ℝ) (z : Grid M) :=
   …

   Mentions: OAI.FourierLLogL.Dyadic.Node, OAI.FourierLLogL.Dyadic.Grid

3. lemma OAI.FourierLLogL.Dyadic.Thermal.dome_prob line 26
4. lemma OAI.FourierLLogL.Dyadic.Thermal.prob_as_ex line 40
5. lemma OAI.FourierLLogL.Dyadic.Thermal.ch_dome_bound line 44
6. lemma OAI.FourierLLogL.Dyadic.Thermal.two_envelope line 71

   Source documentation

   factorization for the two center-shifted weights used in the unconditional cap

   private lemma two_envelope {A B C : Form M} (hA : 0 ≤ A) (hB : 0 ≤ B) (hh : A+B ≤ C)
       (i j s : Grid M) :
       ‖expU (fun y => (↑(boltz A (i-y)*boltz B (j-y)):ℂ)*chi s y)‖ ≤ exp (-F (A+B))*cred C s := by
   …

   Mentions: OAI.FourierLLogL.Dyadic.Thermal.Form, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.expU, OAI.FourierLLogL.Dyadic.Thermal.boltz, OAI.FourierLLogL.Dyadic.chi, OAI.FourierLLogL.Dyadic.Thermal.F, OAI.FourierLLogL.Dyadic.Thermal.cred

7. lemma OAI.FourierLLogL.Dyadic.Thermal.moments_bias line 86
8. lemma OAI.FourierLLogL.Dyadic.Thermal.ex_pow_bound line 110
9. lemma OAI.FourierLLogL.Dyadic.Thermal.uniform_level_cost line 117