TransferFrequencyRigidity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness of the two child frequencies and inserted pivot

theorem OAI.Ostmann.transfer_frequency_determinant_zero line 11

Source documentation

Comparing two valid substitutions makes the child-frequency determinant both divisible by the root frequency and too small to be nonzero.

theorem transfer_frequency_determinant_zero (L R P Q B K : ℕ) (s v w v' w' : ℤ)
    (hs : s ≠ 0) (hunit : IsCoprime s (R : ℤ))
    (hrel : v * R - w * L = s * P) (hrel' : v' * R - w' * L = s * Q)
    (hP : P ≤ K) (hQ : Q ≤ K) (hw : w.natAbs ≤ B) (hw' : w'.natAbs ≤ B)
    (hgap : 2 * K * B < R) : v * w' - v' * w = 0 := by
…

theorem OAI.Ostmann.transfer_substitution_unique line 41

Source documentation

Coprimality with the frequencies rules out any nontrivial proportional rescaling of the positive pivot.

theorem transfer_substitution_unique (L R P Q B K : ℕ) (s v w v' w' : ℤ)
    (hs : s ≠ 0) (hunit : IsCoprime s (R : ℤ))
    (hrel : v * R - w * L = s * P) (hrel' : v' * R - w' * L = s * Q)
    (hPpos : 0 < P) (hP : P ≤ K) (hQ : Q ≤ K)
    (hw : w.natAbs ≤ B) (hw' : w'.natAbs ≤ B)
    (hgap : 2 * K * B < R)
    (hPw : P.Coprime w.natAbs) (hQw : Q.Coprime w'.natAbs) :
    v = v' ∧ w = w' ∧ P = Q := by
…