OAI/Analysis/FourierLLogL/Dyadic/Snap.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Subgrids, snapping and projecting

  1. def OAI.FourierLLogL.Dyadic.times_step line 14
  2. def OAI.FourierLLogL.Dyadic.raise line 20

    Source documentation

    Mesh 2^(M-l) in multiples.

    def raise (h : l ≤ M) : Grid l →+ Grid M :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Grid

  3. def OAI.FourierLLogL.Dyadic.cut line 27
  4. lemma OAI.FourierLLogL.Dyadic.cut_natCast line 30
  5. lemma OAI.FourierLLogL.Dyadic.cut_val line 33
  6. lemma OAI.FourierLLogL.Dyadic.cut_mod line 36
  7. lemma OAI.FourierLLogL.Dyadic.raise_cast line 39
  8. lemma OAI.FourierLLogL.Dyadic.raise_eq line 44
  9. lemma OAI.FourierLLogL.Dyadic.raise_val line 47
  10. lemma OAI.FourierLLogL.Dyadic.raise_inj line 54
  11. lemma OAI.FourierLLogL.Dyadic.raised_pos line 61
  12. lemma OAI.FourierLLogL.Dyadic.cut_chi line 66
  13. lemma OAI.FourierLLogL.Dyadic.annihilator line 76
  14. def OAI.FourierLLogL.Dyadic.down line 91

    Source documentation

    A snap (rounding down).

    def down (_h : l ≤ M) (u : Grid M) : Grid l :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Grid

  15. lemma OAI.FourierLLogL.Dyadic.raise_down line 94
  16. lemma OAI.FourierLLogL.Dyadic.snap_dist line 100
  17. lemma OAI.FourierLLogL.Dyadic.cut_injOn line 108
  18. lemma OAI.FourierLLogL.Dyadic.cut_send line 134

    Source documentation

    Projection density bound for any input sublaw on p.

    lemma cut_send {p : Node} (h : l ≤ M) (hp : p.ok M) (hh : M-l ≤ p.lev)
    (P : Law (Grid M)) (a : ℝ) (ha : 0 ≤ a)
    (H : ∀ x, P x ≤ a*p.dice M x) (i : Grid l) :
    P.send (cut h) i ≤ a*p.invlen*side M := by
…

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