SupportedPivotTransfer.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Pivot transfer with bounds imposed on the actual nonzero support

theorem OAI.Ostmann.pivot_square_split_on_support line 14

Source documentation

The residue identity is needed only for pairs with nonzero coefficients. Thus the original coprimality indicator stays inside the coefficient.

theorem pivot_square_split_on_support {A : Type*} [Fintype A]
    (M : ℕ) [NeZero M] (L : A → ℕ) (v : A → ℤ) (c : A → ℂ)
    (hL : ∀ a, c a ≠ 0 → (L a).Coprime M) :
    (∑ u : Fin M, ‖groupedCoefficient (fun a => pivotResidueKey M (L a) (v a)) c u‖ ^ 2) =
      (pivotDiagonal L v c).re + (pivotOffDiagonal M L v c).re := by
…

Mentions: OAI.Ostmann.groupedCoefficient, OAI.Ostmann.pivotResidueKey, OAI.Ostmann.pivotDiagonal, OAI.Ostmann.pivotOffDiagonal

theorem OAI.Ostmann.pivotDiagonal_nonneg_on_support line 39
theorem OAI.Ostmann.pivotOffDiagonal_frequency_on_support line 64
theorem OAI.Ostmann.pivotDiagonal_nonneg_of_positive_support line 95
Source documentation
Positivity of the active product alone makes the zero-numerator part a square. Frequency size is needed later to identify its prime matching, but is not needed for this nonnegativity step.
```
theorem pivotDiagonal_nonneg_of_positive_support {A : Type*} [Fintype A]
    (L : A → ℕ) (v : A → ℤ) (c : A → ℂ)
    (hpos : ∀ a, c a ≠ 0 → 0 < L a) : 0 ≤ (pivotDiagonal L v c).re := by
…
```
Mentions: OAI.Ostmann.pivotDiagonal

theorem OAI.Ostmann.sum_pivotOffDiagonal_substitution_on_support line 126

Source documentation

This is the extended integer sum with the original support left in its coefficients. Every off-diagonal term has one forced positive pivot.

theorem sum_pivotOffDiagonal_substitution_on_support {A : Type*} [Fintype A]
    (T : Finset ℕ) (hT : ∀ M ∈ T, 0 < M) (B H V : ℕ)
    (L : A → ℕ) (v : A → ℤ) (c : ℕ → A → ℂ)
    (hv : ∀ M ∈ T, ∀ a, c M a ≠ 0 → (v a).natAbs ≤ B)
    (hL : ∀ M ∈ T, ∀ a, c M a ≠ 0 → L a ≤ H)
    (hscale : ∀ M ∈ T, 2 * B * H ≤ V * M) :
    (∑ M ∈ T, pivotOffDiagonal M L v (c M)) =
      ∑ s ∈ transferFrequencyRange V, ∑ a, ∑ b,
        if validTransferredPivot T (v a * L b - v b * L a) s
        then c (reconstructedPivot (v a * L b - v b * L a) s) a *
          conj (c (reconstructedPivot (v a * L b - v b * L a) s) b) else 0 := by
…

Mentions: OAI.Ostmann.pivotOffDiagonal, OAI.Ostmann.transferFrequencyRange, OAI.Ostmann.validTransferredPivot, OAI.Ostmann.reconstructedPivot