MaskedRotations.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Genuine rotations on the retained cyclic cells

The corrected rows have a common initial projection. Cutting them by its orthogonal cells gives actual square-zero partial isometries and hence a connected unitary for any finite collection of angles. The removed cell is absent from both initial rows; the complement of their final ranges is retained. No claim that the ambient zero cell is fixed is made.

def OAI.WeakPureInfiniteness.maskedRotationPiece line 24
Source documentation
The partial isometry between the two copies of a retained cell.
```
def maskedRotationPiece (r t f : E) : E := t * f * star r
…
```
lemma OAI.WeakPureInfiniteness.maskedRotationPiece_relations line 27
lemma OAI.WeakPureInfiniteness.maskedRotationPiece_support_orthogonal line 66

def OAI.WeakPureInfiniteness.maskedRotationUnitary line 95

Source documentation

A finite family of the corrected cell rotations is an actual unitary.

def maskedRotationUnitary (p r t : E) (f : I → E)
    (hr : star r * r = p) (ht : star t * t = p) (hrt : star r * t = 0)
    (hf : ∀ i, IsStarProjection (f i)) (hpf : ∀ i, p * f i = f i)
    (ho : ∀ i j, i ≠ j → f i * f j = 0) (θ : I → ℝ) : unitary E :=
…

lemma OAI.WeakPureInfiniteness.maskedRotationUnitary_zero line 107
lemma OAI.WeakPureInfiniteness.maskedRotationUnitary_continuous line 117
lemma OAI.WeakPureInfiniteness.maskedRotationUnitary_joined line 132
lemma OAI.WeakPureInfiniteness.maskedRotationUnitary_sub_norm_le line 153
def OAI.WeakPureInfiniteness.maskedAngleCos line 167
Source documentation
The two diagonal coefficients of the finite angular profile.
```
def maskedAngleCos (f : I → E) (θ : I → ℝ) : E :=
…
```
def OAI.WeakPureInfiniteness.maskedAngleSin line 170
def OAI.WeakPureInfiniteness.maskedRotationModel line 175
Source documentation
Polynomial comparison expression, also defined for uncorrected rows.
```
def maskedRotationModel (r t c s : E) : E :=
…
```
lemma OAI.WeakPureInfiniteness.maskedRotationUnitary_formula line 179
lemma OAI.WeakPureInfiniteness.masked_weighted_projection_norm line 201
lemma OAI.WeakPureInfiniteness.maskedAngleCos_norm_le line 217
lemma OAI.WeakPureInfiniteness.maskedAngleSin_norm_le line 226
lemma OAI.WeakPureInfiniteness.rotation_sandwich_difference line 232
lemma OAI.WeakPureInfiniteness.maskedRotationModel_sub_norm_le line 253

lemma OAI.WeakPureInfiniteness.retainedCell_properties line 282

Source documentation

Masking a single cell preserves the remaining orthogonal projections.

lemma retainedCell_properties (e : I → E) (o : I)
    (he : ∀ i, IsStarProjection (e i))
    (ho : ∀ i j, i ≠ j → e i * e j = 0) :
    (∀ i, IsStarProjection (maskedBandCoefficients e o i)) ∧
      (∀ i, (1 - e o) * maskedBandCoefficients e o i = maskedBandCoefficients e o i) ∧
      (∀ i j, i ≠ j → maskedBandCoefficients e o i * maskedBandCoefficients e o j = 0) := by
…

Mentions: OAI.WeakPureInfiniteness.maskedBandCoefficients

lemma OAI.WeakPureInfiniteness.relativeInitial_norm_le line 308

lemma OAI.WeakPureInfiniteness.exists_actual_masked_rotation line 321

Source documentation

The rotation unitary is constructed for the actual cyclic partition and masked iterated row words. Its polynomial comparison error is independent of the number of cells. This does not assert the cocycle equation.

lemma exists_actual_masked_rotation (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) (θ : ZMod (2 ^ m) → ℝ) (ε : ℝ) (hε : 0 < ε) :
    ∃ (e : ZMod (2 ^ m) → E) (u : unitary E),
      (∀ j, IsStarProjection (e j)) ∧
      (∀ j k, j ≠ k → e j * e k = 0) ∧ (∑ j, e j) = 1 ∧
      Joined (1 : unitary E) u ∧
      ‖(u : E) - maskedRotationModel
        (maskedTowerBand e (Equiv.addRight 2)
          (fun j => finiteRowShiftIterate s j.val (s 0 * s 0)) 0)
        (maskedTowerBand e (Equiv.addRight 1)
…

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