OAI/Computability/FourierCircuit/Boundary.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Literal relation between modulus multiplication and the supported correction. This is the missing interface at 06-feedback:86--196, not an assumed theorem. Noncommutative coefficient matrices remain ordered J_i G_j.

  1. def OAI.ExactFourier.Boundary.quotientLinear line 10
  2. theorem OAI.ExactFourier.Boundary.quotientLinear_apply line 26
  3. theorem OAI.ExactFourier.Boundary.prefix_quotient_zero line 30

    Source documentation

    Inputs strictly before the final d times do not cross the coefficient boundary.

    theorem prefix_quotient_zero (ℓ f : ℂ[X]) (hℓ : ℓ.Monic)
    {d t b : ℕ} (ht : ℓ.natDegree = t) (hf : f.natDegree ≤ d) (hb : b + d < t) :
    (f * X ^ b) /ₘ ℓ = 0 := by
…
  4. theorem OAI.ExactFourier.Boundary.quotient_degree_lt line 42

    Source documentation

    The quotient, with sign reversed, has strictly fewer than d coefficients.

    theorem quotient_degree_lt (ℓ f : ℂ[X]) (hℓ : ℓ.Monic)
    {d t b : ℕ} (ht : ℓ.natDegree = t) (hd : 0 < d)
    (hf : f.natDegree ≤ d) (hb : b < t) :
    ((f * X ^ b) /ₘ ℓ).natDegree < d := by
…
  5. theorem OAI.ExactFourier.Boundary.quotient_shift_expansion line 53

    Source documentation

    Exact division of a shifted matrix entry. This keeps the generator coefficients on the left, ready for the ordered J_i*G_j matrix formula.

    theorem quotient_shift_expansion (ℓ f : ℂ[X]) (hℓ : ℓ.Monic)
    {d : ℕ} (hf : f.natDegree ≤ d) (b : ℕ) :
    (f * X ^ b) /ₘ ℓ =
      ∑ j ∈ Finset.range (d + 1), f.coeff j • ((X ^ (b + j) : ℂ[X]) /ₘ ℓ) := by
…
  6. theorem OAI.ExactFourier.Boundary.boundary_difference line 72

    Source documentation

    Entrywise modulus reduction differs from time truncation by minus the modulus times precisely the quotient above. No bounds on coefficients are imposed.

    theorem boundary_difference (ℓ f : ℂ[X]) (b : ℕ) :
    (f * X ^ b) %ₘ ℓ - f * X ^ b = -ℓ * ((f * X ^ b) /ₘ ℓ) := by
…
  7. def OAI.ExactFourier.Boundary.timeMatrix line 77
  8. def OAI.ExactFourier.Boundary.modulusMatrix line 81
  9. theorem OAI.ExactFourier.Boundary.correction_prefix_zero line 86

    Source documentation

    The modulus correction has no columns at times b<t-d.

    theorem correction_prefix_zero {ι : Type} {t d : ℕ} (G : Matrix ι ι ℂ[X])
    (ℓ : ℂ[X]) (hℓ : ℓ.Monic) (ht : ℓ.natDegree = t)
    (hG : ∀ i j, (G i j).natDegree ≤ d)
    (a b : Fin t × ι) (hb : b.1.val < t - d) :
    (modulusMatrix t ℓ G - timeMatrix t G) a b = 0 := by
…

    Mentions: OAI.ExactFourier.Boundary.modulusMatrix, OAI.ExactFourier.Boundary.timeMatrix

  10. def OAI.ExactFourier.Boundary.orderedWeight line 98

    Source documentation

    Scalar weights for the exact ordered generator formula. Prefix correction uses η=1. The suffix uses the first t coefficients of ℓ/u^k.

    noncomputable def orderedWeight (η ℓ : ℂ[X]) (a b i j : ℕ) : ℂ :=
…
  11. theorem OAI.ExactFourier.Boundary.polynomial_ordered_expansion line 101
  12. def OAI.ExactFourier.Boundary.coefficientMatrix line 119
  13. def OAI.ExactFourier.Boundary.weightedCorrection line 124

    Source documentation

    Polynomial correction for a single input time b, before taking its output coefficient. Matrix multiplication is in the original order J then G.

    noncomputable def weightedCorrection {ι : Type} [Fintype ι] (η ℓ : ℂ[X])
    (J G : Matrix ι ι ℂ[X]) (b : ℕ) : Matrix ι ι ℂ[X] :=
…
  14. theorem OAI.ExactFourier.Boundary.ordered_span line 130

    Source documentation

    Exact ordered-span part of the coefficient-boundary comparison. There is no commutation hypothesis on any pair of spatial coefficient matrices.

    theorem ordered_span {ι : Type} [Fintype ι] (η ℓ : ℂ[X]) (hℓ : ℓ.Monic)
    (J G : Matrix ι ι ℂ[X]) {d e : ℕ}
    (hG : ∀ u v, (G u v).natDegree ≤ d)
    (hJ : ∀ u v, (J u v).natDegree ≤ e) (a b : ℕ) :
    coefficientMatrix (weightedCorrection η ℓ J G b) a =
      ∑ i ∈ Finset.range (e+1), ∑ j ∈ Finset.range (d+1),
        orderedWeight η ℓ a b i j • (coefficientMatrix J i * coefficientMatrix G j) := by
…

    Mentions: OAI.ExactFourier.Boundary.coefficientMatrix, OAI.ExactFourier.Boundary.weightedCorrection, OAI.ExactFourier.Boundary.orderedWeight

  15. theorem OAI.ExactFourier.Boundary.orderedWeight_prefix line 155

    Source documentation

    Explicit prefix coefficient convention, including negative (a-i) indices.

    theorem orderedWeight_prefix (ℓ : ℂ[X]) (a b i j : ℕ) :
    orderedWeight 1 ℓ a b i j =
      if i ≤ a then -((X ^ (b+j) : ℂ[X]) /ₘ ℓ).coeff (a-i) else 0 := by
…

    Mentions: OAI.ExactFourier.Boundary.orderedWeight

  16. theorem OAI.ExactFourier.Boundary.prefix_row_vanishes line 162

    Source documentation

    The prefix correction J*v has no coefficients at times a>=e+d.

    theorem prefix_row_vanishes {ι : Type} [Fintype ι] (ℓ : ℂ[X]) (hℓ : ℓ.Monic)
    (J G : Matrix ι ι ℂ[X]) {d e t a b : ℕ}
    (ht : ℓ.natDegree = t) (hd : 0 < d)
    (hG : ∀ u v, (G u v).natDegree ≤ d)
    (hJ : ∀ u v, (J u v).natDegree ≤ e)
    (hb : b < t) (ha : e+d ≤ a) :
    coefficientMatrix (weightedCorrection 1 ℓ J G b) a = 0 := by
…

    Mentions: OAI.ExactFourier.Boundary.coefficientMatrix, OAI.ExactFourier.Boundary.weightedCorrection

  17. theorem OAI.ExactFourier.Boundary.weightedCorrection_prefix_zero line 183

    Source documentation

    No weighted correction has an input column before the suffix.

    theorem weightedCorrection_prefix_zero {ι : Type} [Fintype ι]
    (η ℓ : ℂ[X]) (hℓ : ℓ.Monic) (J G : Matrix ι ι ℂ[X]) {d t b : ℕ}
    (ht : ℓ.natDegree = t) (hG : ∀ u v, (G u v).natDegree ≤ d)
    (hb : b+d < t) : weightedCorrection η ℓ J G b = 0 := by
…

    Mentions: OAI.ExactFourier.Boundary.weightedCorrection

  18. def OAI.ExactFourier.Boundary.activeCorrection line 196

    Source documentation

    The actual early--suffix formula after the scalar prefix conjugation.

    noncomputable def activeCorrection {ι : Type} [Fintype ι]
    (t d : ℕ) (η ℓ : ℂ[X]) (J G : Matrix ι ι ℂ[X]) :
    Matrix (Fin t × ι) (Fin t × ι) ℂ := fun a b =>
…
  19. def OAI.ExactFourier.Boundary.ActiveTime line 203
  20. instance OAI.ExactFourier.Boundary.(instance at line 205) line 205
  21. theorem OAI.ExactFourier.Boundary.activeCorrection_column_support line 209
  22. theorem OAI.ExactFourier.Boundary.activeCorrection_row_support line 220
  23. theorem OAI.ExactFourier.Boundary.supported_identity_decomposition line 236

    Source documentation

    Simultaneous row/column permutation isolates every matrix correction supported on a single active index set, with an exact identity on its complement.

    theorem supported_identity_decomposition {κ : Type} [DecidableEq κ]
    (S : κ → Prop) [DecidablePred S] (L : Matrix κ κ ℂ)
    (hrow : ∀ i j, ¬S i → L i j = 0)
    (hcol : ∀ i j, ¬S j → L i j = 0) :
    (1 + L).submatrix (Equiv.sumCompl S) (Equiv.sumCompl S) =
      Matrix.fromBlocks (1 + L.submatrix Subtype.val Subtype.val)
        (0 : Matrix {i // S i} {i // ¬S i} ℂ) 0 1 := by
…

    Mentions: OAI.ExactFourier.L

  24. theorem OAI.ExactFourier.Boundary.active_identity_decomposition line 252
  25. def OAI.ExactFourier.Boundary.seriesMatrix line 284
  26. theorem OAI.ExactFourier.Boundary.seriesMatrix_apply line 288
  27. theorem OAI.ExactFourier.Boundary.timeMatrix_eq_trunc line 291
  28. def OAI.ExactFourier.Boundary.quotientColumns line 298
  29. theorem OAI.ExactFourier.Boundary.difference_eq_columns line 303

    Source documentation

    The exact remainder-minus-truncation map: minus the quotient times ℓ.

    theorem difference_eq_columns {ι : Type} [Fintype ι] [DecidableEq ι]
    (t : ℕ) (ℓ : ℂ[X]) (G : Matrix ι ι ℂ[X]) :
    modulusMatrix t ℓ G - timeMatrix t G =
      coefficientColumns t ((ℓ : PowerSeries ℂ) • quotientColumns t ℓ G) := by
…

    Mentions: OAI.ExactFourier.Boundary.modulusMatrix, OAI.ExactFourier.Boundary.timeMatrix, OAI.ExactFourier.Boundary.quotientColumns

  30. theorem OAI.ExactFourier.Boundary.timeMatrix_inverse line 319

    Source documentation

    The polynomial adjugate/denominator identity gives the TRUE inverse, before any support reduction. This is not an inverse evaluation assumption.

    theorem timeMatrix_inverse {ι : Type} [Fintype ι] [DecidableEq ι]
    (t : ℕ) (u : ℂ[X]) (G J : Matrix ι ι ℂ[X])
    (hu : u.coeff 0 ≠ 0) (hGJ : G * J = Matrix.scalar ι u) :
    (timeMatrix t G)⁻¹ =
      blockTruncHom t ((u : PowerSeries ℂ)⁻¹ • seriesMatrix J) := by
…

    Mentions: OAI.ExactFourier.Boundary.timeMatrix, OAI.ExactFourier.Boundary.seriesMatrix

  31. theorem OAI.ExactFourier.Boundary.inverse_mul_difference line 339

    Source documentation

    The relative correction is the coefficient map of (ℓ/u) J v, with the quotient sign included in v.

    theorem inverse_mul_difference {ι : Type} [Fintype ι] [DecidableEq ι]
    (t : ℕ) (u ℓ : ℂ[X]) (G J : Matrix ι ι ℂ[X])
    (hu : u.coeff 0 ≠ 0) (hGJ : G * J = Matrix.scalar ι u) :
    (timeMatrix t G)⁻¹ * (modulusMatrix t ℓ G - timeMatrix t G) =
      coefficientColumns t (((ℓ : PowerSeries ℂ) * (u : PowerSeries ℂ)⁻¹) •
        (seriesMatrix J * quotientColumns t ℓ G)) := by
…

    Mentions: OAI.ExactFourier.Boundary.timeMatrix, OAI.ExactFourier.Boundary.modulusMatrix, OAI.ExactFourier.Boundary.seriesMatrix, OAI.ExactFourier.Boundary.quotientColumns

  32. theorem OAI.ExactFourier.Boundary.prefix_scalar_cancels line 351

    Source documentation

    A prefix-only scalar convolution cancels the denominator on early rows, and literally leaves the late rows unchanged.

    theorem prefix_scalar_cancels {ι κ : Type} [Fintype ι] [DecidableEq ι]
    (t T : ℕ) (f η : PowerSeries ℂ) (hfη : f*η=1)
    (V : Matrix ι κ (PowerSeries ℂ)) (a : Fin t × ι) (b : κ) :
    ((prefixScalar t T f ⊗ₖ (1 : Matrix ι ι ℂ)) *
      coefficientColumns t (η • V)) a b =
        if a.1.val < T then PowerSeries.coeff a.1.val (V a.2 b)
        else PowerSeries.coeff a.1.val (η * V a.2 b) := by
…
  33. theorem OAI.ExactFourier.Boundary.coeff_trunc_mul_series line 368

    Source documentation

    Coefficients below t cannot see the discarded tail of a scalar series.

    theorem coeff_trunc_mul_series (t : ℕ) (η V : PowerSeries ℂ) (a : Fin t) :
    PowerSeries.coeff a.val (((PowerSeries.trunc t η : ℂ[X]) : PowerSeries ℂ) * V) =
      PowerSeries.coeff a.val (η*V) := by
…
  34. theorem OAI.ExactFourier.Boundary.weightedCorrection_series line 381

    Source documentation

    Converting the finite polynomial ordered generator formula to series changes neither matrix order nor the sign of the quotient.

    theorem weightedCorrection_series {ι : Type} [Fintype ι] [DecidableEq ι]
    (t : ℕ) (η ℓ : ℂ[X]) (J G : Matrix ι ι ℂ[X])
    (i : ι) (b : Fin t × ι) :
    (((weightedCorrection η ℓ J G b.1.val) i b.2 : ℂ[X]) : PowerSeries ℂ) =
      (η : PowerSeries ℂ) * (seriesMatrix J * quotientColumns t ℓ G) i b := by
…

    Mentions: OAI.ExactFourier.Boundary.weightedCorrection, OAI.ExactFourier.Boundary.seriesMatrix, OAI.ExactFourier.Boundary.quotientColumns

  35. theorem OAI.ExactFourier.Boundary.weightedCorrection_trunc_coeff line 391

    Source documentation

    The finite polynomial η used in the ordered-span certificate is exactly the first t coefficients of ℓ/u; no truncation error survives in any output row.

    theorem weightedCorrection_trunc_coeff {ι : Type} [Fintype ι] [DecidableEq ι]
    (t : ℕ) (η : PowerSeries ℂ) (ℓ : ℂ[X]) (J G : Matrix ι ι ℂ[X])
    (a b : Fin t × ι) :
    (weightedCorrection (PowerSeries.trunc t η) ℓ J G b.1.val a.2 b.2).coeff a.1.val =
      PowerSeries.coeff a.1.val (η * (seriesMatrix J * quotientColumns t ℓ G) a.2 b) := by
…

    Mentions: OAI.ExactFourier.Boundary.weightedCorrection, OAI.ExactFourier.Boundary.seriesMatrix, OAI.ExactFourier.Boundary.quotientColumns

  36. theorem OAI.ExactFourier.Boundary.quotientColumns_prefix_zero line 401

    Source documentation

    Quotient columns vanish on the whole coefficient prefix, not merely on an assumed active direct summand.

    theorem quotientColumns_prefix_zero {ι : Type} (t d : ℕ) (ℓ : ℂ[X])
    (hℓ : ℓ.Monic) (ht : ℓ.natDegree=t) (G : Matrix ι ι ℂ[X])
    (hG : ∀ i j, (G i j).natDegree ≤ d) (i : ι) (b : Fin t × ι)
    (hb : b.1.val < t-d) : quotientColumns t ℓ G i b = 0 := by
…

    Mentions: OAI.ExactFourier.Boundary.quotientColumns

  37. theorem OAI.ExactFourier.Boundary.inverse_difference_prefix_zero line 410

    Source documentation

    The actual relative map I+S is fixed on its right by every prefix map.

    theorem inverse_difference_prefix_zero {ι : Type} [Fintype ι] [DecidableEq ι]
    (t d : ℕ) (u ℓ : ℂ[X]) (G J : Matrix ι ι ℂ[X])
    (hu : u.coeff 0 ≠ 0) (hGJ : G*J=Matrix.scalar ι u)
    (hℓ : ℓ.Monic) (ht : ℓ.natDegree=t) (hG : ∀ i j, (G i j).natDegree ≤ d)
    (a b : Fin t × ι) (hb : b.1.val < t-d) :
    ((timeMatrix t G)⁻¹ * (modulusMatrix t ℓ G - timeMatrix t G)) a b = 0 := by
…

    Mentions: OAI.ExactFourier.Boundary.timeMatrix, OAI.ExactFourier.Boundary.modulusMatrix

  38. theorem OAI.ExactFourier.Boundary.prefix_mul_inverse_difference line 423

    Source documentation

    Premultiplication of the literal relative correction gives exactly the previously certified finite activeCorrection matrix.

    theorem prefix_mul_inverse_difference {ι : Type} [Fintype ι] [DecidableEq ι]
    (t d : ℕ) (u ℓ : ℂ[X]) (G J : Matrix ι ι ℂ[X])
    (hu : u.coeff 0 ≠ 0) (hℓ0 : ℓ.coeff 0 ≠ 0)
    (hGJ : G*J=Matrix.scalar ι u) :
    (prefixScalar t (t-d) ((u : PowerSeries ℂ) * (ℓ : PowerSeries ℂ)⁻¹) ⊗ₖ
      (1 : Matrix ι ι ℂ)) *
      ((timeMatrix t G)⁻¹ * (modulusMatrix t ℓ G - timeMatrix t G)) =
        activeCorrection t d
          (PowerSeries.trunc t ((ℓ : PowerSeries ℂ) * (u : PowerSeries ℂ)⁻¹)) ℓ J G := by
…

    Mentions: OAI.ExactFourier.Boundary.timeMatrix, OAI.ExactFourier.Boundary.modulusMatrix, OAI.ExactFourier.Boundary.activeCorrection

  39. theorem OAI.ExactFourier.Boundary.prefix_conjugated_relative_map line 455