DyadicChord.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SmoothObstruction.DyadicChord.prefixSum line 14
def OAI.SmoothObstruction.DyadicChord.average line 15
def OAI.SmoothObstruction.DyadicChord.chord line 16
def OAI.SmoothObstruction.DyadicChord.deviation line 17
lemma OAI.SmoothObstruction.DyadicChord.prefixSum_add line 20
lemma OAI.SmoothObstruction.DyadicChord.deviation_nonneg line 24
lemma OAI.SmoothObstruction.DyadicChord.abs_chord_le line 31
lemma OAI.SmoothObstruction.DyadicChord.deviation_le line 39
lemma OAI.SmoothObstruction.DyadicChord.deviation_one line 46
lemma OAI.SmoothObstruction.DyadicChord.average_double line 52
lemma OAI.SmoothObstruction.DyadicChord.prefixSum_eq line 58
lemma OAI.SmoothObstruction.DyadicChord.chord_left line 64
lemma OAI.SmoothObstruction.DyadicChord.chord_right line 69
lemma OAI.SmoothObstruction.DyadicChord.deviation_double_le line 78
Source documentation
A deterministic midpoint recurrence for maximal deviation from the block's own chord. No independence or average mixing hypothesis is used.
```
lemma deviation_double_le (f : ℕ → ℝ) {n : ℕ} (hn : 0 < n) :
    deviation f (2 * n) ≤
      (|average f n - average f (2 * n)| +
        max (deviation f n) (deviation (fun j => f (n + j)) n)) / 2 := by
…
```
Mentions: OAI.SmoothObstruction.DyadicChord.deviation, OAI.SmoothObstruction.DyadicChord.average
lemma OAI.SmoothObstruction.DyadicChord.deviation_double_sq line 131
Source documentation
A rational square version, more convenient for summing the L² energies.
```
lemma deviation_double_sq (f : ℕ → ℝ) {n : ℕ} (hn : 0 < n) :
    (deviation f (2 * n))^2 ≤
      (3 / 4 : ℝ) * (average f n - average f (2 * n))^2 +
      (3 / 8 : ℝ) * ((deviation f n)^2 + (deviation (fun j => f (n + j)) n)^2) := by
…
```
Mentions: OAI.SmoothObstruction.DyadicChord.deviation, OAI.SmoothObstruction.DyadicChord.average
lemma OAI.SmoothObstruction.DyadicChord.prefixSum_memLp line 155
lemma OAI.SmoothObstruction.DyadicChord.average_memLp line 159
lemma OAI.SmoothObstruction.DyadicChord.chord_memLp line 163
lemma OAI.SmoothObstruction.DyadicChord.deviation_memLp line 167
def OAI.SmoothObstruction.DyadicChord.orbit line 185
Source documentation
A measure-preserving transformation gives precisely the stationarity needed below; no independence, ergodicity, or decay of correlations enters.
```
def orbit (T : Ω → Ω) (f : Ω → ℝ) (x : Ω) (j : ℕ) : ℝ := f (T^[j] x)
…
```
lemma OAI.SmoothObstruction.DyadicChord.orbit_shift line 188
lemma OAI.SmoothObstruction.DyadicChord.integral_comp_preserving line 193
lemma OAI.SmoothObstruction.DyadicChord.orbit_memLp line 203
def OAI.SmoothObstruction.DyadicChord.averageEnergy line 207
def OAI.SmoothObstruction.DyadicChord.deviationEnergy line 210
lemma OAI.SmoothObstruction.DyadicChord.averageEnergy_nonneg line 213
lemma OAI.SmoothObstruction.DyadicChord.deviationEnergy_nonneg line 216
lemma OAI.SmoothObstruction.DyadicChord.deviationEnergy_one line 219
lemma OAI.SmoothObstruction.DyadicChord.averageEnergy_one line 222
lemma OAI.SmoothObstruction.DyadicChord.averageEnergy_shift line 226
lemma OAI.SmoothObstruction.DyadicChord.deviationEnergy_shift line 232
lemma OAI.SmoothObstruction.DyadicChord.midpoint_energy line 240
Source documentation
The midpoint square is exactly the drop in the average's second moment. This identity uses only stationarity of the right half.
```
lemma midpoint_energy {T : Ω → Ω} (hT : MeasurePreserving T μ μ) {f : Ω → ℝ}
    (hf : MemLp f 2 μ) {n : ℕ} (hn : 0 < n) :
    (∫ x, (average (orbit T f x) n - average (orbit T f x) (2 * n))^2 ∂μ) =
      averageEnergy T f μ n - averageEnergy T f μ (2 * n) := by
…
```
Mentions: OAI.SmoothObstruction.DyadicChord.average, OAI.SmoothObstruction.DyadicChord.orbit, OAI.SmoothObstruction.DyadicChord.averageEnergy
lemma OAI.SmoothObstruction.DyadicChord.averageEnergy_double_le line 267
lemma OAI.SmoothObstruction.DyadicChord.deviationEnergy_double line 275

lemma OAI.SmoothObstruction.DyadicChord.energy_sum_bound line 312

Source documentation

A telescoping potential turns the midpoint recurrence into an absolute summability bound. These constants do not depend on a process or dimension.

lemma energy_sum_bound (A Z : ℕ → ℝ) (hA : ∀ h, 0 ≤ A h) (hZ : ∀ h, 0 ≤ Z h)
    (hZ₀ : Z 0 = 0)
    (hrec : ∀ h, Z (h + 1) ≤ (3 / 4 : ℝ) * (A h - A (h + 1)) + (3 / 4 : ℝ) * Z h)
    (N : ℕ) : ∑ h ∈ range N, Z h ≤ 3 * A 0 := by
…

lemma OAI.SmoothObstruction.DyadicChord.energy_summable line 325
theorem OAI.SmoothObstruction.DyadicChord.dyadic_square_summable line 338
Source documentation
The square-summability conclusion of the source dyadic chord lemma, with an explicit absolute constant 3. The process is recorded as an observable of a measure-preserving transformation; in particular it covers the compact orthogonal-frame process required by the smooth switching construction.
```
theorem dyadic_square_summable {T : Ω → Ω} (hT : MeasurePreserving T μ μ)
    {f : Ω → ℝ} (hf : MemLp f 2 μ) :
    Summable (fun h => deviationEnergy T f μ (2^h)) ∧
      (∑' h, deviationEnergy T f μ (2^h)) ≤ 3 * ∫ x, (f x)^2 ∂μ := by
…
```
Mentions: OAI.SmoothObstruction.DyadicChord.deviationEnergy

theorem OAI.SmoothObstruction.DyadicChord.average_drop_summable line 352

Source documentation

The nonnegative drops in the second moments telescope, without any need for an ergodic theorem or for a mixing estimate.

theorem average_drop_summable {T : Ω → Ω} (hT : MeasurePreserving T μ μ)
    {f : Ω → ℝ} (hf : MemLp f 2 μ) :
    (∀ h, 0 ≤ averageEnergy T f μ (2^h) - averageEnergy T f μ (2^(h + 1))) ∧
    Summable (fun h => averageEnergy T f μ (2^h) - averageEnergy T f μ (2^(h + 1))) ∧
    (∑' h, (averageEnergy T f μ (2^h) - averageEnergy T f μ (2^(h + 1)))) ≤
      ∫ x, (f x)^2 ∂μ := by
…

Mentions: OAI.SmoothObstruction.DyadicChord.averageEnergy