OAI/Analysis/FourierLLogL/Thermal/Piece.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Finite input pieces and spectra, using counting measure for the observation coordinate

  1. def OAI.FourierLLogL.Dyadic.Node.child line 14
  2. lemma OAI.FourierLLogL.Dyadic.Node.child_ok line 17
  3. lemma OAI.FourierLLogL.Dyadic.Node.child_len line 19
  4. lemma OAI.FourierLLogL.Dyadic.Node.child_below line 21
  5. def OAI.FourierLLogL.Dyadic.Thermal.channel line 30

    Source documentation

    Observation type-A.

    def channel (A : Form M) (x : Grid M) : Law (Grid M) :=
…

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

  6. lemma OAI.FourierLLogL.Dyadic.Thermal.channel_apply line 33
  7. lemma OAI.FourierLLogL.Dyadic.Thermal.ch_K line 39
  8. lemma OAI.FourierLLogL.Dyadic.Thermal.ch_pos line 42
  9. lemma OAI.FourierLLogL.Dyadic.Thermal.ch_ex line 44
  10. lemma OAI.FourierLLogL.Dyadic.Thermal.ch_noise line 47
  11. def OAI.FourierLLogL.Dyadic.Thermal.wt line 52

    Source documentation

    Local normalized subdensity (as mass weights, counting-grid). Its total is m/α.

    def wt (p : Node) (a : Grid M → ℝ) (α : ℝ) (y : Grid M) : ℝ :=
…

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

  12. lemma OAI.FourierLLogL.Dyadic.Thermal.wt_nonneg line 55
  13. lemma OAI.FourierLLogL.Dyadic.Thermal.wt_total line 58
  14. def OAI.FourierLLogL.Dyadic.Thermal.PieceLaw line 63

    Source documentation

    Law of a local piece when normalization is its positive mean; used as proof-carrying relation to any specified law.

    def PieceLaw (p : Node) (a : Grid M → ℝ) (P : Law (Grid M)) := ∀ y, P y = wt p a (p.avg a) y

    Mentions: OAI.FourierLLogL.Dyadic.Node, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Law, OAI.FourierLLogL.Dyadic.Thermal.wt

  15. lemma OAI.FourierLLogL.Dyadic.Thermal.make_piece line 65
  16. lemma OAI.FourierLLogL.Dyadic.Thermal.piece_support line 69
  17. lemma OAI.FourierLLogL.Dyadic.Thermal.piece_density line 75
  18. lemma OAI.FourierLLogL.Dyadic.Thermal.wt_half line 88
  19. def OAI.FourierLLogL.Dyadic.Thermal.omegaObs line 98

    Source documentation

    Observation law weighted by the local subpiece.

    def omegaObs (p : Node) (a : Grid M → ℝ) (α : ℝ) (A : Form M) (y z : Grid M) :=
…

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

  20. def OAI.FourierLLogL.Dyadic.Thermal.Mz line 100
  21. def OAI.FourierLLogL.Dyadic.Thermal.fz line 102
  22. def OAI.FourierLLogL.Dyadic.Thermal.energyZ line 104
  23. def OAI.FourierLLogL.Dyadic.Thermal.high line 107
  24. lemma OAI.FourierLLogL.Dyadic.Thermal.density_nonneg line 110
  25. lemma OAI.FourierLLogL.Dyadic.Thermal.mass_nonneg line 114
  26. lemma OAI.FourierLLogL.Dyadic.Thermal.mass_total line 118
  27. lemma OAI.FourierLLogL.Dyadic.Thermal.fz_norm line 123
  28. lemma OAI.FourierLLogL.Dyadic.Thermal.energyZ_le line 130
  29. def OAI.FourierLLogL.Dyadic.Thermal.polar line 140
  30. lemma OAI.FourierLLogL.Dyadic.Thermal.polar_identity line 142
  31. lemma OAI.FourierLLogL.Dyadic.Thermal.polar_unit line 151
  32. lemma OAI.FourierLLogL.Dyadic.Thermal.piece_child_bias line 157