CancellationBandwidth.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The three homogeneous components of the cancellation path

The explicit two-corner cancellation has a diagonal part and two opposite off-diagonal parts. For corners of degrees differing by one, these have total degrees 0, -1 and 1. This finite formula is the input needed before transporting a fragmentation path through cyclic towers.

lemma OAI.WeakPureInfiniteness.compression_mul_isometry line 20
lemma OAI.WeakPureInfiniteness.compression_mul_orthogonal line 29

lemma OAI.WeakPureInfiniteness.cornerRotation_mul_second line 35

Source documentation

The second range rotates into the first with the stated sign.

lemma cornerRotation_mul_second (a b : E)
    (ha : star a * a = 1) (hb : star b * b = 1)
    (hab : star a * b = 0) (θ : ℝ) :
    partialIsometryBergRotation (b * star a) θ * b =
      (Real.cos θ) • b - (Real.sin θ) • a := by
…

Mentions: OAI.WeakPureInfiniteness.partialIsometryBergRotation

lemma OAI.WeakPureInfiniteness.compression_two_vector_formula line 51

lemma OAI.WeakPureInfiniteness.cornerCancellationPath_three_terms line 82

Source documentation

Exact finite-band formula for the actual cancellation path. The two nonzero-degree coefficients are negatives of one another's adjoints.

lemma cornerCancellationPath_three_terms (a b u : E)
    (ha : star a * a = 1) (hb : star b * b = 1)
    (hab : star a * b = 0) (hu : u * star u = 1) (θ : ℝ) :
    cornerCancellationPath a b u θ =
      1 + (Real.cos θ ^ 2) •
        (a * (u - 1) * star a + b * (star u - 1) * star b) +
      (Real.sin θ * Real.cos θ) •
        (a * (u - 1) * star b - b * (star u - 1) * star a) := by
…

Mentions: OAI.WeakPureInfiniteness.cornerCancellationPath

lemma OAI.WeakPureInfiniteness.cornerCancellationPath_phase line 108

Source documentation

Under a phase on the first corner and no phase on the second, the actual path has only the constant, positive and negative phase terms. This states the phase hypotheses explicitly; it does not assume that a cyclic tower commutes with the path.

lemma cornerCancellationPath_phase (a b u : E)
    (ha : star a * a = 1) (hb : star b * b = 1)
    (hab : star a * b = 0) (hu : u * star u = 1)
    (φ : E →⋆ₐ[ℂ] E) (ζ : ℂ) (hζ : ζ * star ζ = 1)
    (hφa : φ a = ζ • a) (hφb : φ b = b) (hφu : φ u = u) (θ : ℝ) :
    φ (cornerCancellationPath a b u θ) =
      1 + (Real.cos θ ^ 2) •
        (a * (u - 1) * star a + b * (star u - 1) * star b) +
      (Real.sin θ * Real.cos θ) •
        (ζ • (a * (u - 1) * star b) -
          star ζ • (b * (star u - 1) * star a)) := by
…

Mentions: OAI.WeakPureInfiniteness.cornerCancellationPath