Crossings.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Selected period crossings and finite-dimensional obstruction.

structure OAI.DoublingHilbert.ColorBlock line 18
Source documentation
One full period, recording its integral horizontal and vertical origins.
```
structure ColorBlock (j : ℕ) where
…
```
def OAI.DoublingHilbert.ColorBlock.rectangle line 25
def OAI.DoublingHilbert.ColorBlock.column line 31
def OAI.DoublingHilbert.ColorBlock.row line 34
theorem OAI.DoublingHilbert.ColorBlock.column_subset line 37
theorem OAI.DoublingHilbert.ColorBlock.row_subset line 41
theorem OAI.DoublingHilbert.ColorBlock.column_color line 45
theorem OAI.DoublingHilbert.ColorBlock.row_color line 54
theorem OAI.DoublingHilbert.ColorBlock.x_length line 63
theorem OAI.DoublingHilbert.ColorBlock.y_length line 68
theorem OAI.DoublingHilbert.ColorBlock.row_energy_le line 72
theorem OAI.DoublingHilbert.ColorBlock.column_energy_le line 78
def OAI.DoublingHilbert.PeriodGrid.colorBlock line 89
theorem OAI.DoublingHilbert.PeriodGrid.block_eq_colorBlock line 92

theorem OAI.DoublingHilbert.exists_horizontal_line line 111

Source documentation

Fubini selects a genuine interior horizontal line with an all-points oscillation bound.

theorem exists_horizontal_line (I J : Segment) {F G : Base → E} {C C' : NNReal}
    (hF : LipschitzWith C F) (hG : LipschitzWith C' G)
    {e : Base → ℝ} (he : IsBoundedField e) {c : ℝ} (hc : 0 ≤ c)
    (hdom : ∀ y ∈ Ioo J.lo J.hi, ∀ x : ℝ,
      c * ‖column G (1, 0) (x, y) - column F (1, 0) (x, y)‖ ^ 2 ≤ e (x, y)) :
    ∃ y ∈ Ioo J.lo J.hi, ∀ a ∈ Icc I.lo I.hi, ∀ b ∈ Icc I.lo I.hi,
      c * ‖(G (b, y) - F (b, y)) - (G (a, y) - F (a, y))‖ ^ 2 ≤
        I.length ^ 2 * (∫ p, e p ∂(Rectangle.mk I J).law) := by
…

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

theorem OAI.DoublingHilbert.exists_vertical_line line 148

Source documentation

The independent vertical-line selection, with the same avoidance of FTC null sets.

theorem exists_vertical_line (I J : Segment) {F G : Base → E} {C C' : NNReal}
    (hF : LipschitzWith C F) (hG : LipschitzWith C' G)
    {e : Base → ℝ} (he : IsBoundedField e) {c : ℝ} (hc : 0 ≤ c)
    (hdom : ∀ x ∈ Ioo I.lo I.hi, ∀ y : ℝ,
      c * ‖column G (0, 1) (x, y) - column F (0, 1) (x, y)‖ ^ 2 ≤ e (x, y)) :
    ∃ x ∈ Ioo I.lo I.hi, ∀ a ∈ Icc J.lo J.hi, ∀ b ∈ Icc J.lo J.hi,
      c * ‖(G (x, b) - F (x, b)) - (G (x, a) - F (x, a))‖ ^ 2 ≤
        J.length ^ 2 * (∫ p, e p ∂(Rectangle.mk I J).law) := by
…

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

theorem OAI.DoublingHilbert.exists_small_energy_block line 193
Source documentation
Finite averaging chooses one complete period without increasing the mean energy.
```
theorem exists_small_energy_block {f : constructedSet → E} {D : NNReal}
    (hf : LipschitzWith D f) (N : ℕ) (hN : 0 < N) {η : ℝ} (hη : 0 < η) :
    ∃ (w : Tuple) (j : ℕ) (B : ColorBlock j), colors j = N ∧ w j = 0 ∧
      B.rectangle.closed ⊆ sheetDomain w ∧
      (∫ p, combinedEnergy hf w j p ∂B.rectangle.law) < η := by
…
```
Mentions: OAI.DoublingHilbert.constructedSet, OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.ColorBlock, OAI.DoublingHilbert.colors, OAI.DoublingHilbert.sheetDomain, OAI.DoublingHilbert.combinedEnergy

theorem OAI.DoublingHilbert.exists_color_row line 207

Source documentation

Every color has a selected horizontal line; the anisotropic weight is retained.

theorem exists_color_row {f : constructedSet → E} {D : NNReal}
    (hf : LipschitzWith D f) (w : Tuple) (j : ℕ) (B : ColorBlock j)
    (i : Fin (colors j)) :
    ∃ y ∈ Ioo (B.row i).lo (B.row i).hi,
      ∀ a ∈ Icc B.rectangle.x.lo B.rectangle.x.hi,
      ∀ b ∈ Icc B.rectangle.x.lo B.rectangle.x.hi,
      (widthFactor j : ℝ) ^ 2 *
        ‖(addedSheet hf w j i (b, y) - globalSheet hf w (b, y)) -
          (addedSheet hf w j i (a, y) - globalSheet hf w (a, y))‖ ^ 2 ≤
        B.rectangle.x.length ^ 2 *
          (colors j * (∫ p, combinedEnergy hf w j p ∂B.rectangle.law)) := by
…

Mentions: OAI.DoublingHilbert.constructedSet, OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.ColorBlock, OAI.DoublingHilbert.colors, OAI.DoublingHilbert.widthFactor, OAI.DoublingHilbert.addedSheet, OAI.DoublingHilbert.globalSheet, OAI.DoublingHilbert.combinedEnergy

theorem OAI.DoublingHilbert.exists_color_column line 236

Source documentation

Independently select an interior vertical line for each color.

theorem exists_color_column {f : constructedSet → E} {D : NNReal}
    (hf : LipschitzWith D f) (w : Tuple) (j : ℕ) (B : ColorBlock j)
    (i : Fin (colors j)) :
    ∃ x ∈ Ioo (B.column i).lo (B.column i).hi,
      ∀ a ∈ Icc B.rectangle.y.lo B.rectangle.y.hi,
      ∀ b ∈ Icc B.rectangle.y.lo B.rectangle.y.hi,
        ‖(addedSheet hf w j i (x, b) - globalSheet hf w (x, b)) -
          (addedSheet hf w j i (x, a) - globalSheet hf w (x, a))‖ ^ 2 ≤
        B.rectangle.y.length ^ 2 *
          (colors j * (∫ p, combinedEnergy hf w j p ∂B.rectangle.law)) := by
…

Mentions: OAI.DoublingHilbert.constructedSet, OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.ColorBlock, OAI.DoublingHilbert.colors, OAI.DoublingHilbert.addedSheet, OAI.DoublingHilbert.globalSheet, OAI.DoublingHilbert.combinedEnergy

theorem OAI.DoublingHilbert.small_oscillation_of_weighted_energy line 269

Source documentation

The horizontal weight cancels exactly against the longer period side.

theorem small_oscillation_of_weighted_energy {n w r s e : ℝ}
    (hn : 0 < n) (hw : 0 < w) (hr : 0 < r) (hs : 0 ≤ s)
    (he : e ≤ 1 / (64 * n ^ 3))
    (hbound : w ^ 2 * s ^ 2 ≤ (n * w * r) ^ 2 * (n * e)) : s ≤ r / 8 := by
…

theorem OAI.DoublingHilbert.exists_separated_family line 288

Source documentation

Crossings of the selected lines force arbitrarily large separated families in the fixed radius-D target ball. The lower bound is the genuine source distance.

theorem exists_separated_family {f : constructedSet → E} {D : NNReal}
    (hf : LipschitzWith D f) (hlower : ∀ p q, dist p q ≤ dist (f p) (f q))
    (N : ℕ) (hN : 0 < N) :
    ∃ z : Fin N → E, (∀ i, ‖z i‖ ≤ D) ∧
      ∀ i m, i ≠ m → 1 ≤ dist (z i) (z m) := by
…

Mentions: OAI.DoublingHilbert.constructedSet