OAI/Analysis/FourierLLogL/Thermal/Shrink.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Iterated spectral compression

  1. def OAI.FourierLLogL.Dyadic.Thermal.supported line 16
  2. def OAI.FourierLLogL.Dyadic.Thermal.evenly line 18
  3. lemma OAI.FourierLLogL.Dyadic.Thermal.exists_uniform_sub line 21
  4. lemma OAI.FourierLLogL.Dyadic.Thermal.represent_law line 37
  5. def OAI.FourierLLogL.Dyadic.Thermal.averageCost line 50

    Source documentation

    averaged defect form.

    def averageCost (hl : l ≤ M) (p : Law (Grid l)) (x : Grid l) : Form M :=
…

    Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Thermal.Form

  6. lemma OAI.FourierLLogL.Dyadic.Thermal.averageCost_pos line 53
  7. lemma OAI.FourierLLogL.Dyadic.Thermal.average_form line 56
  8. def OAI.FourierLLogL.Dyadic.Thermal.shrinkScale line 63
  9. lemma OAI.FourierLLogL.Dyadic.Thermal.spectral_compression line 66
  10. lemma OAI.FourierLLogL.Dyadic.Thermal.choose_compression line 126