SparseSplitting.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Spectral norm bounds imply sparse endpoint assignments. The input is a bounded convolution operator with its coefficient formula.

abbrev OAI.Dixmier.ScalarL2 line 19
def OAI.Dixmier.indicatorL2 line 21
theorem OAI.Dixmier.indicatorL2_apply line 23
theorem OAI.Dixmier.indicatorL2_norm_sq line 29
theorem OAI.Dixmier.indicatorL2_norm line 33
def OAI.Dixmier.rectangleEdges line 38

theorem OAI.Dixmier.indicator_convolution_inner line 42

Source documentation

Pairing convolution with the two indicator vectors counts labelled edges.

theorem indicator_convolution_inner (s : I → G)
    (A : ScalarL2 G →L[ℂ] ScalarL2 G)
    (hA : ∀ (ξ : ScalarL2 G) (x : G), A ξ x = ∑ i, ξ (x * s i))
    (U V : Finset G) :
    ⟪indicatorL2 U, A (indicatorL2 V)⟫_ℂ = (rectangleEdges s U V).card := by
…

Mentions: OAI.Dixmier.ScalarL2, OAI.Dixmier.indicatorL2, OAI.Dixmier.rectangleEdges

theorem OAI.Dixmier.rectangleEdges_card_le line 58

Source documentation

The rectangular edge-count bound with all multiplicities retained.

theorem rectangleEdges_card_le (s : I → G)
    (A : ScalarL2 G →L[ℂ] ScalarL2 G)
    (hA : ∀ (ξ : ScalarL2 G) (x : G), A ξ x = ∑ i, ξ (x * s i))
    {q : ℝ} (hq : ‖A‖ ≤ q) (U V : Finset G) :
    ((rectangleEdges s U V).card : ℝ) ≤ q * Real.sqrt ((U.card : ℝ) * V.card) := by
…

Mentions: OAI.Dixmier.ScalarL2, OAI.Dixmier.rectangleEdges

theorem OAI.Dixmier.edges_subset_endpoint_rectangle line 77
Source documentation
Every finite edge family lies in the rectangle of its endpoints.
```
theorem edges_subset_endpoint_rectangle (s : I → G) (F : Finset (G × I)) :
    F ⊆ rectangleEdges s (F.image Prod.fst) (F.image fun e => e.1 * s e.2) := by
…
```
Mentions: OAI.Dixmier.rectangleEdges
theorem OAI.Dixmier.sqrt_mul_le_half_add line 84
Source documentation
Arithmetic used in the Hall argument, including its factor one half.
```
theorem sqrt_mul_le_half_add {u v : ℝ} (hu : 0 ≤ u) (hv : 0 ≤ v) :
    Real.sqrt (u * v) ≤ (u + v) / 2 := by
…
```

theorem OAI.Dixmier.endpoint_density_of_rectangle_bound line 92

Source documentation

The finite Hall density follows from the rectangular spectral estimate.

theorem endpoint_density_of_rectangle_bound (s : I → G) {q : ℝ} {r : ℕ}
    (hq : 0 ≤ q) (hqr : q ≤ r)
    (hrect : ∀ U V : Finset G, ((rectangleEdges s U V).card : ℝ) ≤
      q * Real.sqrt ((U.card : ℝ) * V.card))
    (F : Finset (G × I)) :
    F.card ≤ r * ((F.image Prod.fst).card + (F.image fun e => e.1 * s e.2).card) := by
…

Mentions: OAI.Dixmier.rectangleEdges

theorem OAI.Dixmier.sparse_mask_of_convolution_bound line 114

Source documentation

Sparse assignment from a bounded convolution operator, at any integer capacity above its norm.

theorem sparse_mask_of_convolution_bound (s : I → G)
    (A : ScalarL2 G →L[ℂ] ScalarL2 G)
    (hA : ∀ (ξ : ScalarL2 G) (x : G), A ξ x = ∑ i, ξ (x * s i))
    {r : ℕ} (hr : ‖A‖ ≤ r) :
    ∃ a : G → I → Bool, (∀ x, (rowOnes a x).card ≤ r) ∧
      ∀ y, (columnZeros a s y).card ≤ r := by
…

Mentions: OAI.Dixmier.ScalarL2, OAI.Dixmier.rowOnes, OAI.Dixmier.columnZeros