OAI/Analysis/FourierLLogL/Dyadic/Grid.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

The finite spatial model

  1. abbrev OAI.FourierLLogL.Dyadic.Grid line 13
  2. def OAI.FourierLLogL.Dyadic.pos line 15
  3. def OAI.FourierLLogL.Dyadic.chi line 17
  4. lemma OAI.FourierLLogL.Dyadic.chi_cast line 19
  5. lemma OAI.FourierLLogL.Dyadic.norm_chi line 28
  6. def OAI.FourierLLogL.Dyadic.expU line 33

    Source documentation

    Uniform probability average.

    def expU {E : Type*} [SMul ℝ E] [AddCommMonoid E] {M : ℕ} (f : Grid M → E) :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Grid

  7. structure OAI.FourierLLogL.Dyadic.Node line 36
  8. def OAI.FourierLLogL.Dyadic.Node.root line 43
  9. def OAI.FourierLLogL.Dyadic.Node.valid line 45
  10. def OAI.FourierLLogL.Dyadic.Node.len line 47
  11. def OAI.FourierLLogL.Dyadic.Node.a line 49
  12. def OAI.FourierLLogL.Dyadic.Node.cells line 51
  13. theorem OAI.FourierLLogL.Dyadic.Node.len_pos line 53
  14. lemma OAI.FourierLLogL.Dyadic.Node.cells_sub line 55
  15. lemma OAI.FourierLLogL.Dyadic.Node.cells_dis line 58
  16. def OAI.FourierLLogL.Dyadic.Node.L line 67
  17. def OAI.FourierLLogL.Dyadic.Node.R line 68
  18. lemma OAI.FourierLLogL.Dyadic.Node.len_L line 70
  19. lemma OAI.FourierLLogL.Dyadic.Node.len_R line 71
  20. lemma OAI.FourierLLogL.Dyadic.Node.a_L line 73
  21. lemma OAI.FourierLLogL.Dyadic.Node.a_R line 79
  22. lemma OAI.FourierLLogL.Dyadic.Node.cells_L line 85
  23. lemma OAI.FourierLLogL.Dyadic.Node.cells_R line 86
  24. lemma OAI.FourierLLogL.Dyadic.Node.cells_split line 90
  25. lemma OAI.FourierLLogL.Dyadic.Node.valid_L line 94
  26. lemma OAI.FourierLLogL.Dyadic.Node.valid_R line 96
  27. def OAI.FourierLLogL.Dyadic.Node.block line 99
  28. def OAI.FourierLLogL.Dyadic.Node.avg line 101
  29. def OAI.FourierLLogL.Dyadic.Node.normarg line 104
  30. def OAI.FourierLLogL.Dyadic.Node.Hi line 106
  31. def OAI.FourierLLogL.Dyadic.Node.Gi line 107
  32. lemma OAI.FourierLLogL.Dyadic.Node.arg_mem line 109
  33. lemma OAI.FourierLLogL.Dyadic.Node.argL_eq line 112
  34. lemma OAI.FourierLLogL.Dyadic.Node.argR_eq line 115
  35. lemma OAI.FourierLLogL.Dyadic.Node.Gi_eq line 120
  36. lemma OAI.FourierLLogL.Dyadic.Node.Hi_L line 123
  37. lemma OAI.FourierLLogL.Dyadic.Node.Hi_R line 128
  38. lemma OAI.FourierLLogL.Dyadic.Node.Hi_out line 133
  39. lemma OAI.FourierLLogL.Dyadic.Node.Gi_out line 137
  40. def OAI.FourierLLogL.Dyadic.vertex line 145
  41. def OAI.FourierLLogL.Dyadic.atom line 147
  42. lemma OAI.FourierLLogL.Dyadic.pos_mem line 149
  43. lemma OAI.FourierLLogL.Dyadic.atom_sub line 152
  44. lemma OAI.FourierLLogL.Dyadic.atom_disjoint line 155
  45. lemma OAI.FourierLLogL.Dyadic.atom_measurable line 162
  46. lemma OAI.FourierLLogL.Dyadic.atom_volume line 164
  47. lemma OAI.FourierLLogL.Dyadic.atom_partition line 168
  48. lemma OAI.FourierLLogL.Dyadic.coarse_const line 189

    Source documentation

    Every atom fully inside/out of a coarser dyadic cell.

    lemma coarse_const {p q : Node} (h : p.lev ≤ q.lev) {x y : ℝ}
    (hx : x ∈ q.cells) (hy : y ∈ q.cells) : x ∈ p.cells ↔ y ∈ p.cells := by
…

    Mentions: OAI.FourierLLogL.Dyadic.Node

  49. lemma OAI.FourierLLogL.Dyadic.atom_iff_coarse line 217
  50. lemma OAI.FourierLLogL.Dyadic.Hi_const line 221
  51. lemma OAI.FourierLLogL.Dyadic.Gi_const line 230
  52. def OAI.FourierLLogL.Dyadic.FinJump line 234
  53. def OAI.FourierLLogL.Dyadic.FinShift line 237
  54. def OAI.FourierLLogL.Dyadic.finMod line 240
  55. def OAI.FourierLLogL.Dyadic.finGood line 243
  56. def OAI.FourierLLogL.Dyadic.GridBound line 248

    Source documentation

    Finite cut statement; asks for an L¹ majorant restricted to points where density steps stay below threshold. There is no dependence on a frequency or depth cutoff in the constant.

    def GridBound : Prop :=
…