Energy.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Anisotropic energy bounds and arbitrarily small-energy period grids.

theorem OAI.DoublingHilbert.norm_sub_sq_le_two line 16

Source documentation

A squared triangle inequality with the same reference vector.

theorem norm_sub_sq_le_two {E : Type*} [NormedAddCommGroup E] (a b c : E) :
    ‖a - b‖ ^ 2 ≤ 2 * ‖a - c‖ ^ 2 + 2 * ‖b - c‖ ^ 2 := by
…

theorem OAI.DoublingHilbert.norm_mean_sub_le_of_energy line 27
theorem OAI.DoublingHilbert.energy_sub_le_two line 38
def OAI.DoublingHilbert.horizontalEnergy line 56
def OAI.DoublingHilbert.verticalEnergy line 60
def OAI.DoublingHilbert.combinedEnergy line 64
theorem OAI.DoublingHilbert.bounded_baseColumn line 69
theorem OAI.DoublingHilbert.bounded_horizontalEnergy line 76
theorem OAI.DoublingHilbert.bounded_verticalEnergy line 82
theorem OAI.DoublingHilbert.bounded_combinedEnergy line 88
theorem OAI.DoublingHilbert.combinedEnergy_nonneg line 94
def OAI.DoublingHilbert.horizontalCoefficient line 109
def OAI.DoublingHilbert.verticalCoefficient line 110
theorem OAI.DoublingHilbert.horizontalCoefficient_pos line 112
theorem OAI.DoublingHilbert.verticalCoefficient_pos line 116

theorem OAI.DoublingHilbert.anisotropic_energy_bound line 126

Source documentation

Finite-epsilon anisotropic energy estimates.

theorem anisotropic_energy_bound {f : constructedSet → E} {D : NNReal}
    (hf : LipschitzWith D f) (w : Tuple) (j : ℕ) (hj : w j = 0)
    (G : PeriodGrid j) (hQ : G.rectangle.closed ⊆ sheetDomain w)
    {A B C ε t : ℝ} (hC : 0 ≤ C) (ht : 0 ≤ t) (ht1 : t ≤ 1)
    (hfirst : ∀ z ∈ derivativeCompact f, z.1 ≤ A)
    (hbarrier : ∀ z ∈ derivativeCompact f, z.2 ≤ B + ε + C * (A - z.1))
    (u v : E) (hu : ‖u‖ ≤ 2 * D) (hv : ‖v‖ ≤ 2 * D)
    (hnearu : A - ‖u‖ ^ 2 ≤ t) (hnearv : B - ‖v‖ ^ 2 ≤ t)
    (hbaseu : (∫ p, ‖column (globalSheet hf w) (1, 0) p - u‖ ^ 2 ∂G.rectangle.law) ≤ t ^ 2)
    (hbasev : (∫ p, ‖column (globalSheet hf w) (0, 1) p - v‖ ^ 2 ∂G.rectangle.law) ≤ t ^ 2)
    (hrx : scale j / G.rectangle.x.length ≤ t)
    (hry : scale j / G.rectangle.y.length ≤ t) :
…

Mentions: OAI.DoublingHilbert.constructedSet, OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.PeriodGrid, OAI.DoublingHilbert.sheetDomain, OAI.DoublingHilbert.derivativeCompact, OAI.DoublingHilbert.column, OAI.DoublingHilbert.globalSheet, OAI.DoublingHilbert.scale

theorem OAI.DoublingHilbert.exists_nearmax_grid line 220

Source documentation

Good points near the lexicographic pair and recurrence give actual fine grid rectangles.

theorem exists_nearmax_grid {f : constructedSet → E} {D : NNReal}
    (hf : LipschitzWith D f) (N W : ℕ) (hN : 0 < N) (hW : 0 < W)
    {A B : ℝ} (hAB : (A, B) ∈ derivativeCompact f) {t : ℝ} (ht : 0 < t) :
    ∃ (w : Tuple) (j : ℕ) (G : PeriodGrid j) (u v : E),
      colors j = N ∧ widthFactor j = W ∧ w j = 0 ∧
      G.rectangle.closed ⊆ sheetDomain w ∧
      ‖u‖ ≤ 2 * D ∧ ‖v‖ ≤ 2 * D ∧
      A - ‖u‖ ^ 2 ≤ t ∧ B - ‖v‖ ^ 2 ≤ t ∧
      (∫ p, ‖column (globalSheet hf w) (1, 0) p - u‖ ^ 2 ∂G.rectangle.law) ≤ t ^ 2 ∧
      (∫ p, ‖column (globalSheet hf w) (0, 1) p - v‖ ^ 2 ∂G.rectangle.law) ≤ t ^ 2 ∧
      scale j / G.rectangle.x.length ≤ t ∧ scale j / G.rectangle.y.length ≤ t := by
…

Mentions: OAI.DoublingHilbert.constructedSet, OAI.DoublingHilbert.derivativeCompact, OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.PeriodGrid, OAI.DoublingHilbert.colors, OAI.DoublingHilbert.widthFactor, OAI.DoublingHilbert.sheetDomain, OAI.DoublingHilbert.column, OAI.DoublingHilbert.globalSheet, OAI.DoublingHilbert.scale

theorem OAI.DoublingHilbert.exists_energy_parameters line 297
Source documentation
The order of choices is essential: the strip width follows the compact barrier, then the base error and the unused radius are made small.
```
theorem exists_energy_parameters {D C η : ℝ} (hD : 0 ≤ D) (hC : 0 ≤ C) (hη : 0 < η) :
    ∃ W : ℕ, 0 < W ∧ ∃ t : ℝ, 0 < t ∧ t ≤ 1 ∧
      2 * (η / 8) + 16 * C * D ^ 2 / (W : ℝ) +
        ((W : ℝ) ^ 2 * horizontalCoefficient D + verticalCoefficient D C) * t < η := by
…
```
Mentions: OAI.DoublingHilbert.horizontalCoefficient, OAI.DoublingHilbert.verticalCoefficient
theorem OAI.DoublingHilbert.exists_small_energy_grid line 330
Source documentation
The full analytic output: arbitrarily small combined energy on actual sheets of the single fixed Hilbert set, at a level with any prescribed number of colors.
```
theorem exists_small_energy_grid {f : constructedSet → E} {D : NNReal}
    (hf : LipschitzWith D f) (N : ℕ) (hN : 0 < N) {η : ℝ} (hη : 0 < η) :
    ∃ (w : Tuple) (j : ℕ) (G : PeriodGrid j), colors j = N ∧ w j = 0 ∧
      G.rectangle.closed ⊆ sheetDomain w ∧
      (∫ p, combinedEnergy hf w j p ∂G.rectangle.law) < η := by
…
```
Mentions: OAI.DoublingHilbert.constructedSet, OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.PeriodGrid, OAI.DoublingHilbert.colors, OAI.DoublingHilbert.sheetDomain, OAI.DoublingHilbert.combinedEnergy