Grids.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Fine period grids, energy sampling, and sheet separation.

def OAI.DoublingHilbert.stripColor line 16
Source documentation
The measurable periodic selector; boundary values play no role.
```
def stripColor (N : ℕ) (hN : 0 < N) (h t : ℝ) : Fin N :=
…
```
theorem OAI.DoublingHilbert.measurable_stripColor line 22
theorem OAI.DoublingHilbert.inColoredStrip_stripColor line 31
theorem OAI.DoublingHilbert.ae_inColoredStrip_stripColor line 41
theorem OAI.DoublingHilbert.floor_div_of_mem_strip line 46
theorem OAI.DoublingHilbert.stripColor_eq_of_mem_strip line 51

theorem OAI.DoublingHilbert.color_in_block line 59

Source documentation

Each color appears exactly once in a complete period block.

theorem color_in_block (N : ℕ) (hN : 0 < N) {h t : ℝ} (hh : 0 < h)
    (b : ℤ) (i : Fin N)
    (ht : t ∈ Ioo (((b : ℝ) * N + i) * h) (((b : ℝ) * N + i + 1) * h)) :
    stripColor N hN h t = i ∧ inColoredStrip h N i t := by
…

Mentions: OAI.DoublingHilbert.stripColor, OAI.DoublingHilbert.inColoredStrip

theorem OAI.DoublingHilbert.scale_tendsto_zero line 72
theorem OAI.DoublingHilbert.exists_fine_level line 78
Source documentation
Recurrence supplies arbitrarily fine unused levels with any prescribed pair.
```
theorem exists_fine_level (N W : ℕ) (hN : 0 < N) (hW : 0 < W) (w : Tuple)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ j, colors j = N ∧ widthFactor j = W ∧ w j = 0 ∧ scale j < ε := by
…
```
Mentions: OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.colors, OAI.DoublingHilbert.widthFactor, OAI.DoublingHilbert.scale

theorem OAI.DoublingHilbert.Segment.exists_grid_inside line 93

Source documentation

Trim an interval to full grid periods, losing at most two periods.

theorem exists_grid_inside (I : Segment) {h : ℝ} (hh : 0 < h)
    (hsmall : h < I.length / 4) :
    ∃ (a : ℤ) (n : ℕ) (hn : 0 < n),
      I.lo ≤ (grid (a * h) h n hh hn).lo ∧
      (grid (a * h) h n hh hn).hi ≤ I.hi ∧
      I.length / 2 ≤ (grid (a * h) h n hh hn).length := by
…

Mentions: OAI.DoublingHilbert.Segment, OAI.DoublingHilbert.Segment.grid, OAI.DoublingHilbert.Segment.length

theorem OAI.DoublingHilbert.Segment.cell_subset_grid line 130
Source documentation
Each component cell lies in its whole grid interval.
```
theorem cell_subset_grid (a h : ℝ) {n : ℕ} (hh : 0 < h) (hn : 0 < n)
    (i : Fin n) :
    Icc (cell a h hh i).lo (cell a h hh i).hi ⊆
      Icc (grid a h n hh hn).lo (grid a h n hh hn).hi := by
…
```
Mentions: OAI.DoublingHilbert.Segment.cell, OAI.DoublingHilbert.Segment.grid

theorem OAI.DoublingHilbert.exists_good_le_integral line 152

Source documentation

First-moment sampling avoiding every specified null exceptional set.

theorem exists_good_le_integral {X : Type*} [MeasurableSpace X] {μ : Measure X}
    [IsProbabilityMeasure μ] {g : X → ℝ} (hg : Integrable g μ)
    {P : X → Prop} (hP : ∀ᵐ x ∂μ, P x) :
    ∃ x, P x ∧ g x ≤ ∫ y, g y ∂μ := by
…

theorem OAI.DoublingHilbert.exists_le_finite_mean line 159
theorem OAI.DoublingHilbert.Segment.ext line 172
theorem OAI.DoublingHilbert.Segment.grid_subdivision line 175
theorem OAI.DoublingHilbert.Segment.cell_period_eq_grid line 183
theorem OAI.DoublingHilbert.Rectangle.exists_column_integral_le line 195
theorem OAI.DoublingHilbert.Rectangle.exists_row_integral_le line 202
theorem OAI.DoublingHilbert.Rectangle.integral_column_le_mul_grid line 209
theorem OAI.DoublingHilbert.Rectangle.integral_row_le_mul_grid line 219

theorem OAI.DoublingHilbert.oscillation_sq_le_segment_energy line 239

Source documentation

An FTC identity on all subintervals controls all points of a line, not just a.e. points.

theorem oscillation_sq_le_segment_energy {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [CompleteSpace E] (I : Segment) {f g : ℝ → E}
    (hg : IsBoundedField g)
    (hFTC : ∀ a b, (∫ x in a..b, g x) = f b - f a)
    {a b : ℝ} (ha : a ∈ Icc I.lo I.hi) (hb : b ∈ Icc I.lo I.hi) :
    ‖f b - f a‖ ^ 2 ≤ I.length ^ 2 * (∫ x, ‖g x‖ ^ 2 ∂I.law) := by
…

Mentions: OAI.DoublingHilbert.Segment, OAI.DoublingHilbert.IsBoundedField

theorem OAI.DoublingHilbert.globalSheet_offset line 293
Source documentation
The new sheet's displacement from the base sheet is at most D r wherever it is permitted.
```
theorem globalSheet_offset {f : constructedSet → E} {D : NNReal}
    (hf : LipschitzWith D f) (w : Tuple) (j : ℕ) (hj : w j = 0) {i : ℕ}
    (hi : i < colors j) {p : Base} (hp : p ∈ sheetDomain w) (hip : allowed j i p) :
    ‖globalSheet hf (w.update j (i + 1)) p - globalSheet hf w p‖ ≤ D * scale j := by
…
```
Mentions: OAI.DoublingHilbert.constructedSet, OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.colors, OAI.DoublingHilbert.Base, OAI.DoublingHilbert.sheetDomain, OAI.DoublingHilbert.allowed, OAI.DoublingHilbert.globalSheet, OAI.DoublingHilbert.scale

theorem OAI.DoublingHilbert.globalSheet_separation_sq line 307

Source documentation

At a crossing two different permitted labels retain their exact Hilbert separation.

theorem globalSheet_separation_sq {f : constructedSet → E} {D : NNReal}
    (hf : LipschitzWith D f) (hlower : ∀ x y, dist x y ≤ dist (f x) (f y))
    (w : Tuple) (j : ℕ) (hj : w j = 0) {i m : ℕ} (him : i ≠ m)
    (hi : i < colors j) (hm : m < colors j) {p : Base} (hp : p ∈ sheetDomain w)
    (hip : allowed j i p) (hmp : allowed j m p) :
    2 * scale j ^ 2 ≤ ‖globalSheet hf (w.update j (i + 1)) p -
      globalSheet hf (w.update j (m + 1)) p‖ ^ 2 := by
…

Mentions: OAI.DoublingHilbert.constructedSet, OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.colors, OAI.DoublingHilbert.Base, OAI.DoublingHilbert.sheetDomain, OAI.DoublingHilbert.allowed, OAI.DoublingHilbert.scale, OAI.DoublingHilbert.globalSheet

theorem OAI.DoublingHilbert.norm_le_on_Icc_of_Ioo line 329

Source documentation

Endpoint bounds on an open real interval extend to its endpoints by continuity.

theorem norm_le_on_Icc_of_Ioo {E : Type*} [NormedAddCommGroup E]
    {g : ℝ → E} (hg : Continuous g) {a b R : ℝ} (hab : a < b)
    (hbound : ∀ x ∈ Ioo a b, ‖g x‖ ≤ R) : ∀ x ∈ Icc a b, ‖g x‖ ≤ R := by
…