OAI/Analysis/FourierLLogL/Thermal/GridFreq.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Applying compression on a subgrid

  1. def OAI.FourierLLogL.Dyadic.Thermal.summesh line 17

    Source documentation

    Sum of coeffs on multiples equals expectation over annihilator

    def summesh (h : l ≤ M) (A : Form M) : ℝ := ∑ i : Grid l, q A (raise h i)

    Mentions: OAI.FourierLLogL.Dyadic.Thermal.Form, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Thermal.q, OAI.FourierLLogL.Dyadic.raise

  2. lemma OAI.FourierLLogL.Dyadic.Thermal.expU_wave line 18
  3. lemma OAI.FourierLLogL.Dyadic.Thermal.summesh_eq line 26
  4. lemma OAI.FourierLLogL.Dyadic.Thermal.summesh_bounds line 47
  5. lemma OAI.FourierLLogL.Dyadic.Thermal.S_one_pos line 74
  6. def OAI.FourierLLogL.Dyadic.Thermal.fq line 77
  7. lemma OAI.FourierLLogL.Dyadic.Thermal.fq_apply line 84
  8. def OAI.FourierLLogL.Dyadic.Thermal.fq_cost line 87
  9. def OAI.FourierLLogL.Dyadic.Thermal.raiseChar line 89
  10. lemma OAI.FourierLLogL.Dyadic.Thermal.raiseChar_eq line 92
  11. lemma OAI.FourierLLogL.Dyadic.Thermal.fq_spec line 95
  12. def OAI.FourierLLogL.Dyadic.Thermal.snapExp line 126

    Source documentation

    Snap parameter l associated with a node and h.

    def snapExp (j : ℕ) (p : Node) :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Node

  13. def OAI.FourierLLogL.Dyadic.Thermal.snapGrid line 128
  14. def OAI.FourierLLogL.Dyadic.Thermal.sig line 129
  15. def OAI.FourierLLogL.Dyadic.Thermal.sepRad line 130
  16. lemma OAI.FourierLLogL.Dyadic.Thermal.snap_le line 132
  17. lemma OAI.FourierLLogL.Dyadic.Thermal.step_scale line 133