TransferOutputSupport.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Coprimality and frequency units after the actual substitution

theorem OAI.Ostmann.transfer_output_support line 11

Source documentation

The common-prime obstruction is impossible once the derived output frequency is smaller than every surviving prime.

theorem transfer_output_support (M L R Y V : ℕ) (v w s : ℤ)
    (hs : s ≠ 0) (hsV : s.natAbs ≤ V)
    (hrel : v * R - w * L = s * M)
    (hLY : L.Coprime Y) (hRY : R.Coprime Y)
    (hlargeL : ∀ q, q.Prime → q ∣ L → V < q)
    (hlargeR : ∀ q, q.Prime → q ∣ R → V < q)
    (hlargeY : ∀ q, q.Prime → q ∣ Y → V < q)
    (hunit : ∀ q, q.Prime → q ∣ L → q ∣ R → IsCoprime (q : ℤ) (M : ℤ)) :
    L.Coprime R ∧ L.Coprime Y ∧ R.Coprime Y ∧
      (L * R * Y).Coprime s.natAbs := by
…

theorem OAI.Ostmann.common_prime_pivot_unit line 33
Source documentation
In the integer extension, the inherited coprimality with the erased pivot implies precisely the common-prime unit condition used above.
```
theorem common_prime_pivot_unit (M L R : ℕ) (hLM : L.Coprime M)
    (q : ℕ) (_hq : q.Prime) (hqL : q ∣ L) (_hqR : q ∣ R) :
    IsCoprime (q : ℤ) (M : ℤ) := by
…
```
theorem OAI.Ostmann.transfer_output_support_of_ranges line 40