OAI/NumberTheory/Ostmann/Construction/TransferPhaseSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.prime_product_factors_large line 12
2. theorem OAI.Ostmann.transfer_copied_support_of_ranges line 22

   Source documentation

   The integer extension keeps its inherited unit conditions. The signed substitution then supplies every support hypothesis of the phase identity.

   theorem transfer_copied_support_of_ranges {H Y : Type*} [Fintype H] [Fintype Y]
       (L R : H → ℕ) (U : Y → ℕ)
       [∀ h, Fact (L h).Prime] [∀ h, Fact (R h).Prime] [∀ y, Fact (U y).Prime]
       (M B K V : ℕ) (v w s : ℤ) (hMpos : 0 < M) (hs : s ≠ 0)
       (hrel : v * (∏ h, R h) - w * (∏ h, L h) = s * M)
       (hv : v.natAbs ≤ B) (hw : w.natAbs ≤ B)
       (hLbound : (∏ h, L h) ≤ K) (hRbound : (∏ h, R h) ≤ K)
       (hscale : 2 * B * K ≤ V * M)
       (hL : Pairwise (fun h k => (L h).Coprime (L k)))
       (hR : Pairwise (fun h k => (R h).Coprime (R k)))
       (hU : Pairwise (fun y z => (U y).Coprime (U z)))
       (hLU : (∏ h, L h).Coprime (∏ y, U y)) (hRU : (∏ h, R h).Coprime (∏ y, U y))
   …

3. theorem OAI.Ostmann.transfer_complete_phase_of_ranges line 54

   Source documentation

   The full phase identity with support derived from the original ranges.

   theorem transfer_complete_phase_of_ranges {H Y : Type*} [Fintype H] [Fintype Y]
       (L R : H → ℕ) (U : Y → ℕ)
       [∀ h, Fact (L h).Prime] [∀ h, Fact (R h).Prime] [∀ y, Fact (U y).Prime]
       (t : ∀ p : ℕ, ZMod p)
       (χH : H → ∀ p : ℕ, DirichletCharacter ℂ p)
       (χY : Y → ∀ p : ℕ, DirichletCharacter ℂ p)
       (b : Option (H ⊕ Y) → Option (H ⊕ Y) → ℤ)
       (νL νR : H → ℂ) (νYL νYR : Y → ℂ) (M : ℕ) (v w s : ℤ)
       (hrel : v * (∏ h, R h) - w * (∏ h, L h) = s * M)
       (B K V : ℕ) (hMpos : 0 < M) (hs : s ≠ 0)
       (hv : v.natAbs ≤ B) (hw : w.natAbs ≤ B)
       (hLbound : (∏ h, L h) ≤ K) (hRbound : (∏ h, R h) ≤ K)
   …