MovingPrimeArithmeticTransfer.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The weighted giant-only integer substitution of Section 7.5

def OAI.Ostmann.movingGiantOffDiagonal line 13
Source documentation
The inserted giant is N / (s * U). The compensation product U is retained, so the reconstructed integer is the giant and not the whole pivot.
```
noncomputable def movingGiantOffDiagonal {A : Type*} [Fintype A]
    (I : Finset ℕ) (V U : ℕ) (L : A → ℕ) (v : A → ℤ)
    (w : ℕ → ℝ) (c : ℕ → A → ℂ) : ℂ :=
…
```

theorem OAI.Ostmann.movingGiantOffDiagonal_eq line 24

Source documentation

The exact weighted off-diagonal, with the original coefficient support and without any multiplicity factor in the integer substitution.

theorem movingGiantOffDiagonal_eq {A : Type*} [Fintype A]
    (I : Finset ℕ) (hI : ∀ p ∈ I, 0 < p) (U : ℕ) (hU : 0 < U)
    (B H V : ℕ) (L : A → ℕ) (v : A → ℤ) (w : ℕ → ℝ) (c : ℕ → A → ℂ)
    (hv : ∀ p ∈ I, ∀ a, c p a ≠ 0 → (v a).natAbs ≤ B)
    (hL : ∀ p ∈ I, ∀ a, c p a ≠ 0 → L a ≤ H)
    (hscale : ∀ p ∈ I, 2 * B * H ≤ V * (p * U)) :
    (∑ p ∈ I, (w p : ℂ) * pivotOffDiagonal (p * U) L v (c p)) =
      movingGiantOffDiagonal I V U L v w c := by
…

Mentions: OAI.Ostmann.pivotOffDiagonal, OAI.Ostmann.movingGiantOffDiagonal