OAI/Analysis/OInfinity/MaskedBandRows.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual iterated rows with the cyclic boundary removed

The zero cell is removed explicitly. On the retained domain, the two neighboring-depth bands have small Gram errors. Their cross term is controlled by the actual inner-letter orthogonality relation, rather than an assumed slow-variation property.

  1. def OAI.WeakPureInfiniteness.maskedBandCoefficients line 20
  2. def OAI.WeakPureInfiniteness.maskedTowerBand line 23
  3. lemma OAI.WeakPureInfiniteness.maskedTowerBand_right_support line 26
  4. lemma OAI.WeakPureInfiniteness.mask_projection_sum line 39
  5. lemma OAI.WeakPureInfiniteness.maskedTowerBand_gram_bound line 53
  6. lemma OAI.WeakPureInfiniteness.iterate_one line 106
  7. lemma OAI.WeakPureInfiniteness.iterate_isometry line 113
  8. lemma OAI.WeakPureInfiniteness.isometry_norm_bound line 120
  9. lemma OAI.WeakPureInfiniteness.maskedIteratedWord_gram_bound line 130

    Source documentation

    A concrete word of degree at most two gives an almost isometric masked band on exactly 1-e₀.

    lemma maskedIteratedWord_gram_bound {N : ℕ} [NeZero N] (s : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hsum : (∑ i, s i * star (s i)) = 1)
    (e : ZMod N → E) (he : ∀ j, IsStarProjection (e j))
    (ho : ∀ i j, i ≠ j → e i * e j = 0) (hesum : (∑ i, e i) = 1)
    (η : ℝ) (hη : 0 ≤ η)
    (hshift : ∀ j, ‖finiteRowShift s (e j) - e (j + 1)‖ ≤ η)
    (x : E) (hx : star x * x = 1) (d : ZMod N)
    (hxshift : ∀ j, ‖x * e j - e (j + d) * x‖ ≤ 2 * η) :
    let A := maskedTowerBand e (Equiv.addRight d)
…

    Mentions: OAI.WeakPureInfiniteness.finiteRowShift, OAI.WeakPureInfiniteness.maskedTowerBand

  10. lemma OAI.WeakPureInfiniteness.maskedIteratedRows_cross_bound line 159

    Source documentation

    The actual two-letter and one-letter bands have small cross Gram on the retained cells. The cyclic zero cell is explicitly removed.

    lemma maskedIteratedRows_cross_bound {N : ℕ} [NeZero N] (hN : 1 < N)
    (s : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (e : ZMod N → E) (he : ∀ j, IsStarProjection (e j))
    (ho : ∀ j k, j ≠ k → e j * e k = 0)
    (η : ℝ) (hη : 0 ≤ η)
    (hshift : ∀ j, ‖finiteRowShift s (e j) - e (j + 1)‖ ≤ η)
    (i r l : Fin 2) (hrl : r ≠ l) :
    let A := maskedTowerBand e (Equiv.addRight 2)
…

    Mentions: OAI.WeakPureInfiniteness.finiteRowShift, OAI.WeakPureInfiniteness.maskedTowerBand