RelativeGramCorrection.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Gram correction with a common initial projection

The removed cyclic cell is not filled. Adding its complementary projection only to the square Gram matrix permits inverse-square-root normalization; the corrected rectangular row still has the original initial projection.

lemma OAI.WeakPureInfiniteness.exists_relative_rectangular_isometry_near line 26

Source documentation

Rectangular normalization preserves an exact right support.

lemma exists_relative_rectangular_isometry_near
    {m n : Type*} [Fintype m] [Fintype n] [DecidableEq n]
    (M ε : ℝ) (hM : 0 ≤ M) (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ (u : CStarMatrix m n E) (q : CStarMatrix n n E),
      IsStarProjection q → u * q = u → ‖u‖ ≤ M →
      ‖u.conjTranspose * u - q‖ < δ →
      ∃ v : CStarMatrix m n E,
        v * q = v ∧ v.conjTranspose * v = q ∧ ‖v - u‖ < ε := by
…

def OAI.WeakPureInfiniteness.relativePairProjection line 106
Source documentation
The common initial projection of a two-column row.
```
def relativePairProjection (p : E) : CStarMatrix (Fin 2) (Fin 2) E :=
…
```
lemma OAI.WeakPureInfiniteness.relativePairProjection_apply line 110
lemma OAI.WeakPureInfiniteness.relativePairProjection_isStarProjection line 114
lemma OAI.WeakPureInfiniteness.cuntzPairRow_relative_support line 128
lemma OAI.WeakPureInfiniteness.cuntzPairRow_relative_gram_bound line 134

lemma OAI.WeakPureInfiniteness.exists_relative_cuntzPair_near line 149

Source documentation

Two approximately orthogonal supported columns can be corrected without filling the removed projection.

lemma exists_relative_cuntzPair_near (ε : ℝ) (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ a b p : E,
      IsStarProjection p → a * p = a → b * p = b → ‖a‖ ≤ 1 → ‖b‖ ≤ 1 →
      ‖star a * a - p‖ < δ → ‖star b * b - p‖ < δ → ‖star a * b‖ < δ →
      ∃ r t : E, r * p = r ∧ t * p = t ∧
        star r * r = p ∧ star t * t = p ∧ star r * t = 0 ∧
        ‖r - a‖ < ε ∧ ‖t - b‖ < ε := by
…

lemma OAI.WeakPureInfiniteness.relativeGram_word_isometry line 184
lemma OAI.WeakPureInfiniteness.relativeGram_iterate_isometry line 193
lemma OAI.WeakPureInfiniteness.relativeGram_isometry_norm line 204

lemma OAI.WeakPureInfiniteness.exists_corrected_masked_binary_rows line 213

Source documentation

The actual iterated two-letter and one-letter bands admit exact relative orthogonalization, with arbitrarily small correction. The cell zero stays removed from both initial projections.

lemma exists_corrected_masked_binary_rows {N : ℕ} [NeZero N] (hN : 1 < N)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ η : ℝ, 0 < η ∧ ∀ (s : Fin 2 → E),
      (∀ i j, star (s i) * s j = if i = j then 1 else 0) →
      (∑ i, s i * star (s i)) = 1 →
      ∀ e : ZMod N → E, (∀ j, IsStarProjection (e j)) →
      (∀ j k, j ≠ k → e j * e k = 0) → (∑ j, e j) = 1 →
      (∀ j, ‖finiteRowShift s (e j) - e (j + 1)‖ ≤ η) →
      let a := maskedTowerBand e (Equiv.addRight 2)
…

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

lemma OAI.WeakPureInfiniteness.exists_masked_binary_rotation_rows line 265

Source documentation

An actual cyclic partition supplies the small Gram errors; no tower or exact orthogonal-row premise is retained in this conclusion.

lemma exists_masked_binary_rotation_rows (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)
    (m : ℕ) (hm : 1 < 2 ^ m) (ε : ℝ) (hε : 0 < ε) :
    ∃ (e : ZMod (2 ^ m) → E) (r t : E),
      (∀ j, IsStarProjection (e j)) ∧
      (∀ j k, j ≠ k → e j * e k = 0) ∧ (∑ j, e j) = 1 ∧
      r * (1 - e 0) = r ∧ t * (1 - e 0) = t ∧
      star r * r = 1 - e 0 ∧ star t * t = 1 - e 0 ∧ star r * t = 0 ∧
      ‖r - maskedTowerBand e (Equiv.addRight 2)
        (fun j => finiteRowShiftIterate s j.val (s 0 * s 0)) 0‖ < ε ∧
      ‖t - maskedTowerBand e (Equiv.addRight 1)
…

Mentions: OAI.WeakPureInfiniteness.maskedTowerBand, OAI.WeakPureInfiniteness.finiteRowShiftIterate