OAI/Analysis/FourierLLogL/Thermal/Power.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Moment calculation on the snapped spectrum

  1. def OAI.FourierLLogL.Dyadic.Thermal.ply line 18

    Source documentation

    Polynomial evaluated at points of the full grid.

    def ply (hl : l ≤ M) (p : Law (Grid l)) (f : Grid l → ℂ) (y : Grid M) :=
…

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

  2. def OAI.FourierLLogL.Dyadic.Thermal.HeatM line 20
  3. def OAI.FourierLLogL.Dyadic.Thermal.levelCost line 22
  4. lemma OAI.FourierLLogL.Dyadic.Thermal.ply_unit line 25
  5. lemma OAI.FourierLLogL.Dyadic.Thermal.ply_one_zero line 28
  6. lemma OAI.FourierLLogL.Dyadic.Thermal.HeatM_bounds line 33
  7. lemma OAI.FourierLLogL.Dyadic.Thermal.heat_exp line 45
  8. lemma OAI.FourierLLogL.Dyadic.Thermal.heat_nonneg line 49
  9. lemma OAI.FourierLLogL.Dyadic.Thermal.Cx_send line 53
  10. lemma OAI.FourierLLogL.Dyadic.Thermal.pack_ply_expand line 65
  11. lemma OAI.FourierLLogL.Dyadic.Thermal.selected_heat line 94
  12. lemma OAI.FourierLLogL.Dyadic.Thermal.weighted_envelope line 110