TransferredPivotSubstitution.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Eliminating the extended integer by its exact signed quotient

def OAI.Ostmann.reconstructedPivot line 13
Source documentation
The positive integer retained by a transferred frequency, when its integrality and range indicators hold.
```
def reconstructedPivot (N s : ℤ) : ℕ := (N / s).toNat
```
theorem OAI.Ostmann.reconstructedPivot_of_eq line 15
def OAI.Ostmann.validTransferredPivot line 19
theorem OAI.Ostmann.validTransferredPivot_of_eq line 22
theorem OAI.Ostmann.validTransferredPivot_equation line 33
theorem OAI.Ostmann.transferred_pivot_substitution line 41
Source documentation
The sum over positive integers has exactly one retained term. This identity is valid for arbitrary coefficients, including all inherited weights.
```
theorem transferred_pivot_substitution (T : Finset ℕ)
    (hT : ∀ M ∈ T, 0 < M) (N s : ℤ) (f : ℕ → ℂ) :
    (∑ M ∈ T, if s ≠ 0 ∧ N = s * M then f M else 0) =
      if validTransferredPivot T N s then f (reconstructedPivot N s) else 0 := by
…
```
Mentions: OAI.Ostmann.validTransferredPivot, OAI.Ostmann.reconstructedPivot

theorem OAI.Ostmann.offDiagonal_pivot_substitution line 62

Source documentation

Expanded copied branches now carry only their reconstructed pivot, with all integer range and sign tests retained as indicators.

theorem offDiagonal_pivot_substitution {A : Type*} [Fintype A]
    (T : Finset ℕ) (hT : ∀ M ∈ T, 0 < M) (S : Finset ℤ)
    (L : A → ℕ) (v : A → ℤ) (c : ℕ → A → ℂ) :
    (∑ M ∈ T, ∑ s ∈ S, ∑ a, ∑ b,
      if s ≠ 0 ∧ v a * L b - v b * L a = s * M then c M a * conj (c M b) else 0) =
    ∑ s ∈ S, ∑ 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.validTransferredPivot, OAI.Ostmann.reconstructedPivot

theorem OAI.Ostmann.sum_pivotOffDiagonal_eq_substitution line 84

Source documentation

The whole extended off-diagonal equals the next arithmetic amplitude. Only the actual reconstructed integer is retained in each term.

theorem sum_pivotOffDiagonal_eq_substitution {A : Type*} [Fintype A]
    (T : Finset ℕ) (hT : ∀ M ∈ T, 0 < M) (B H V : ℕ)
    (L : A → ℕ) (v : A → ℤ) (c : ℕ → A → ℂ)
    (hv : ∀ a, (v a).natAbs ≤ B) (hL : ∀ a, 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