CellBounds.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Two-variable localization bounds

The finite inequalities underlying eq:near-cell-diagonal, eq:all-cell-error, and eq:far-cell-diagonal in the sharp-cutoff argument. The incidence set records which pairs of norm cells meet the product boundary. Both row and column degrees enter the near-boundary bound.

theorem OAI.CubicFirstMoment.cell_incidence_energy line 21

Source documentation

Counting a cell's energy once for each of its incident pairs costs at most the degree bound.

theorem cell_incidence_energy {ι κ : Type*} [DecidableEq ι] [DecidableEq κ]
    (I : Finset ι) (E : Finset (ι × κ)) (a : ι → ℝ) (D : ℕ)
    (hI : ∀ e ∈ E, e.1 ∈ I)
    (hD : ∀ i ∈ I, (E.filter (fun e => e.1 = i)).card ≤ D) :
    (∑ e ∈ E, (a e.1) ^ 2) ≤ (D : ℝ) * ∑ i ∈ I, (a i) ^ 2 := by
…

theorem OAI.CubicFirstMoment.cell_incidence_energy_right line 39

Source documentation

The corresponding column-energy bound.

theorem cell_incidence_energy_right {ι κ : Type*} [DecidableEq ι] [DecidableEq κ]
    (J : Finset κ) (E : Finset (ι × κ)) (b : κ → ℝ) (D : ℕ)
    (hJ : ∀ e ∈ E, e.2 ∈ J)
    (hD : ∀ j ∈ J, (E.filter (fun e => e.2 = j)).card ≤ D) :
    (∑ e ∈ E, (b e.2) ^ 2) ≤ (D : ℝ) * ∑ j ∈ J, (b j) ^ 2 := by
…

theorem OAI.CubicFirstMoment.near_cell_sum_sq line 58

Source documentation

Localizing both variables gives the bounded-degree Cauchy inequality. Only the near pairs are summed, rather than all pairs of cells.

theorem near_cell_sum_sq {ι κ : Type*} [DecidableEq ι] [DecidableEq κ]
    (I : Finset ι) (J : Finset κ) (E : Finset (ι × κ))
    (a : ι → ℝ) (b : κ → ℝ) (D : ℕ)
    (hI : ∀ e ∈ E, e.1 ∈ I) (hJ : ∀ e ∈ E, e.2 ∈ J)
    (hrow : ∀ i ∈ I, (E.filter (fun e => e.1 = i)).card ≤ D)
    (hcol : ∀ j ∈ J, (E.filter (fun e => e.2 = j)).card ≤ D) :
    (∑ e ∈ E, a e.1 * b e.2) ^ 2 ≤
      (D : ℝ) ^ 2 * (∑ i ∈ I, (a i) ^ 2) * ∑ j ∈ J, (b j) ^ 2 := by
…

theorem OAI.CubicFirstMoment.near_cell_sum_le line 79

Source documentation

Unsquaring the near-boundary estimate. The cell masses are L² norms in the application and are thus nonnegative.

theorem near_cell_sum_le {ι κ : Type*} [DecidableEq ι] [DecidableEq κ]
    (I : Finset ι) (J : Finset κ) (E : Finset (ι × κ))
    (a : ι → ℝ) (b : κ → ℝ) (D : ℕ)
    (hI : ∀ e ∈ E, e.1 ∈ I) (hJ : ∀ e ∈ E, e.2 ∈ J)
    (hrow : ∀ i ∈ I, (E.filter (fun e => e.1 = i)).card ≤ D)
    (hcol : ∀ j ∈ J, (E.filter (fun e => e.2 = j)).card ≤ D) :
    (∑ e ∈ E, a e.1 * b e.2) ≤
      (D : ℝ) * Real.sqrt (∑ i ∈ I, (a i) ^ 2) *
        Real.sqrt (∑ j ∈ J, (b j) ^ 2) := by
…

theorem OAI.CubicFirstMoment.cell_mass_sum_sq line 102
Source documentation
Without a near-pair restriction, the sum of cell masses costs the square root of the number of cells on each side.
```
theorem cell_mass_sum_sq {ι : Type*} (I : Finset ι) (a : ι → ℝ) :
    (∑ i ∈ I, a i) ^ 2 ≤ (I.card : ℝ) * ∑ i ∈ I, (a i) ^ 2 := by
…
```

theorem OAI.CubicFirstMoment.all_cell_error_sq line 109

Source documentation

The absolute errors over all cell pairs lose three powers of the square root of the number of cells, as in eq:all-cell-error.

theorem all_cell_error_sq {ι κ : Type*} (I : Finset ι) (J : Finset κ)
    (a : ι → ℝ) (error : ℝ) :
    (∑ i ∈ I, ∑ _j ∈ J, a i * error) ^ 2 ≤
      error ^ 2 * (J.card : ℝ) ^ 2 * (I.card : ℝ) * ∑ i ∈ I, (a i) ^ 2 := by
…