OAI/Analysis/OInfinity/MaskedShift.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Shifting the actual masked bands

Shifting an iterated-word band changes the input mask from cell zero to cell one. Reindexing exposes both exceptional cells explicitly, including the genuine N-th iterate on the cyclic return. No terminal norm estimate is inferred from its support.

  1. def OAI.WeakPureInfiniteness.shiftedMaskedBand line 21

    Source documentation

    The shifted finite sum before reindexing its cyclic variable.

    def shiftedMaskedBand {N : ℕ} [NeZero N] (s : Fin 2 → E)
    (e : ZMod N → E) (d : ZMod N) (x : E) : E :=
…
  2. lemma OAI.WeakPureInfiniteness.maskedShift_triple_bound line 26
  3. lemma OAI.WeakPureInfiniteness.maskedBand_shift_approx line 45

    Source documentation

    The quantitative shift error comes solely from the supplied cyclic projection errors; the word iterate itself shifts exactly.

    lemma maskedBand_shift_approx {N : ℕ} [NeZero 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))
    (d : ZMod N) (x : E) (η : ℝ) (hη : 0 ≤ η)
    (hshift : ∀ j, ‖finiteRowShift s (e j) - e (j + 1)‖ ≤ η) :
    ‖finiteRowShift s (maskedTowerBand e (Equiv.addRight d)
        (fun j => finiteRowShiftIterate s j.val x) 0) - shiftedMaskedBand s e d x‖ ≤
      2 * (N : ℝ) * η * ‖x‖ := by
…

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

  4. lemma OAI.WeakPureInfiniteness.maskedShift_val_predecessor line 84
  5. lemma OAI.WeakPureInfiniteness.maskedShift_val_return line 92
  6. lemma OAI.WeakPureInfiniteness.shiftedMaskedBand_boundary line 100

    Source documentation

    Reindexing exposes the missing cell one and the returned cell zero. The coefficient on cell zero is the actual N-th iterate.

    lemma shiftedMaskedBand_boundary {N : ℕ} [NeZero N] (hN : 1 < N)
    (s : Fin 2 → E) (e : ZMod N → E) (d : ZMod N) (x : E) :
    shiftedMaskedBand s e d x =
      maskedTowerBand e (Equiv.addRight d) (fun j => finiteRowShiftIterate s j.val x) 0 +
        e d * finiteRowShiftIterate s N x * e 0 -
        e (1 + d) * finiteRowShiftIterate s 1 x * e 1 := by
…

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

  7. lemma OAI.WeakPureInfiniteness.maskedBand_shift_boundary_error line 142

    Source documentation

    The complete generator-shift estimate retains both boundary operators.

    lemma maskedBand_shift_boundary_error {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))
    (d : ZMod N) (x : E) (η : ℝ) (hη : 0 ≤ η)
    (hshift : ∀ j, ‖finiteRowShift s (e j) - e (j + 1)‖ ≤ η) :
    ‖finiteRowShift s (maskedTowerBand e (Equiv.addRight d)
        (fun j => finiteRowShiftIterate s j.val x) 0) -
      (maskedTowerBand e (Equiv.addRight d) (fun j => finiteRowShiftIterate s j.val x) 0 +
        e d * finiteRowShiftIterate s N x * e 0 -
        e (1 + d) * finiteRowShiftIterate s 1 x * e 1)‖ ≤ 2 * (N : ℝ) * η * ‖x‖ := by
…

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

  8. lemma OAI.WeakPureInfiniteness.maskedBand_shift_times_bound line 157

    Source documentation

    Multiplication by an angular coefficient controls the two actual boundary pieces through its cell-zero and cell-one components.

    lemma maskedBand_shift_times_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))
    (d : ZMod N) (x c : E) (η : ℝ) (hη : 0 ≤ η)
    (hshift : ∀ j, ‖finiteRowShift s (e j) - e (j + 1)‖ ≤ η) :
    let a := maskedTowerBand e (Equiv.addRight d) (fun j => finiteRowShiftIterate s j.val x) 0
…

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

  9. lemma OAI.WeakPureInfiniteness.projection_mul_masked_sum line 207
  10. lemma OAI.WeakPureInfiniteness.maskedAngle_boundary_bounds line 230

    Source documentation

    The removed cell annihilates both actual angular coefficients. Their cell-one components are bounded by the first retained angle.

    lemma maskedAngle_boundary_bounds {N : ℕ} [NeZero N] (hN : 1 < N)
    (e : ZMod N → E) (he : ∀ i, IsStarProjection (e i))
    (ho : ∀ i j, i ≠ j → e i * e j = 0) (θ : ZMod N → ℝ) :
    e 0 * maskedAngleCos (maskedBandCoefficients e 0) θ = 0 ∧
      e 0 * maskedAngleSin (maskedBandCoefficients e 0) θ = 0 ∧
      ‖e 1 * maskedAngleCos (maskedBandCoefficients e 0) θ‖ ≤ |θ 1| ∧
      ‖e 1 * maskedAngleSin (maskedBandCoefficients e 0) θ‖ ≤ |θ 1| := by
…

    Mentions: OAI.WeakPureInfiniteness.maskedAngleCos, OAI.WeakPureInfiniteness.maskedBandCoefficients, OAI.WeakPureInfiniteness.maskedAngleSin

  11. lemma OAI.WeakPureInfiniteness.maskedBand_shift_sine_error line 255

    Source documentation

    For the actual sine profile, the exceptional-cell term is bounded by the first retained angle, rather than by the norm of a whole projection.

    lemma maskedBand_shift_sine_error {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 : ∀ i j, i ≠ j → e i * e j = 0)
    (d : ZMod N) (x : E) (θ : ZMod N → ℝ) (η : ℝ) (hη : 0 ≤ η)
    (hshift : ∀ j, ‖finiteRowShift s (e j) - e (j + 1)‖ ≤ η) :
    let a := maskedTowerBand e (Equiv.addRight d) (fun j => finiteRowShiftIterate s j.val x) 0
…

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

  12. lemma OAI.WeakPureInfiniteness.maskedBand_shift_cosine_error line 275

    Source documentation

    The cosine-minus-one profile has the same actual boundary control.

    lemma maskedBand_shift_cosine_error {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 : ∀ i j, i ≠ j → e i * e j = 0)
    (d : ZMod N) (x : E) (θ : ZMod N → ℝ) (η : ℝ) (hη : 0 ≤ η)
    (hshift : ∀ j, ‖finiteRowShift s (e j) - e (j + 1)‖ ≤ η) :
    let a := maskedTowerBand e (Equiv.addRight d) (fun j => finiteRowShiftIterate s j.val x) 0
…

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