CellGeometry.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Geometry of the product-boundary cells

After scaling log-norm by the cell width, the two norm cells are unit intervals. A pair meeting a width-one strip around the product boundary can lie on only five integer diagonals. This proves the bounded-neighbor claim used in eq:near-cell-diagonal rather than postulating it.

def OAI.CubicFirstMoment.nearCellOffsets line 19
theorem OAI.CubicFirstMoment.nearCellOffsets_card line 21

theorem OAI.CubicFirstMoment.nearCell_index_mem line 26

Source documentation

A cell pair that meets the boundary strip has one of five index sums.

theorem nearCell_index_mem {i j : ℤ} {x y c : ℝ}
    (hx : (i : ℝ) ≤ x ∧ x ≤ (i : ℝ) + 1)
    (hy : (j : ℝ) ≤ y ∧ y ≤ (j : ℝ) + 1)
    (hnear : |x + y - c| ≤ 1) : i + j ∈ nearCellOffsets c := by
…

Mentions: OAI.CubicFirstMoment.nearCellOffsets

theorem OAI.CubicFirstMoment.nearCell_row_degree line 42
theorem OAI.CubicFirstMoment.nearCell_column_degree line 57

theorem OAI.CubicFirstMoment.near_product_boundary_bound line 73

Source documentation

The product-boundary diagonal bound with an absolute constant.

theorem near_product_boundary_bound (I J : Finset ℤ) (E : Finset (ℤ × ℤ))
    (a b : ℤ → ℝ) (c : ℝ) (hI : ∀ e ∈ E, e.1 ∈ I) (hJ : ∀ e ∈ E, e.2 ∈ J)
    (hE : ∀ e ∈ E, ∃ x y : ℝ,
      (e.1 : ℝ) ≤ x ∧ x ≤ (e.1 : ℝ) + 1 ∧
      (e.2 : ℝ) ≤ y ∧ y ≤ (e.2 : ℝ) + 1 ∧ |x + y - c| ≤ 1) :
    (∑ e ∈ E, a e.1 * b e.2) ≤
      5 * Real.sqrt (∑ i ∈ I, (a i) ^ 2) * Real.sqrt (∑ j ∈ J, (b j) ^ 2) := by
…