OAI/NumberTheory/Ostmann/Arithmetic/CRTLineProbabilities.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.uniform_indicator_probability line 11
2. theorem OAI.Ostmann.crt_unit_lines_probability line 22

   Source documentation

   In the prime environment every feasible local line contributes exactly 1/(p-1), and the factors multiply over all distinct internal primes.

   theorem crt_unit_lines_probability {I : Type*} [Fintype I] [DecidableEq I]
       (p : I → ℕ) [∀ i, Fact (p i).Prime] [∀ i, NeZero (p i)] [NeZero (∏ i, p i)]
       (hc : Pairwise (fun i j => (p i).Coprime (p j)))
       (a b : ∀ i, (ZMod (p i))ˣ) :
       (Fintype.card ((ZMod (∏ i, p i))ˣ × (ZMod (∏ i, p i))ˣ) : ℝ)⁻¹ *
         (∑ z, ∏ i, if a i * (crtUnitPairEquiv p hc z i).1 =
             b i * (crtUnitPairEquiv p hc z i).2 then (1 : ℝ) else 0) =
       ∏ i, (Fintype.card (ZMod (p i))ˣ : ℝ)⁻¹ := by
   …

   Mentions: OAI.Ostmann.crtUnitPairEquiv

3. theorem OAI.Ostmann.crt_external_lines_probability line 39

   Source documentation

   In the external-integer environment every feasible line contributes 1/p, including a zero second coefficient.

   theorem crt_external_lines_probability {I : Type*} [Fintype I] [DecidableEq I]
       (p : I → ℕ) [∀ i, Fact (p i).Prime] [∀ i, NeZero (p i)] [NeZero (∏ i, p i)]
       (hc : Pairwise (fun i j => (p i).Coprime (p j)))
       (a : ∀ i, (ZMod (p i))ˣ) (b : ∀ i, ZMod (p i)) :
       (Fintype.card (ZMod (∏ i, p i) × (ZMod (∏ i, p i))ˣ) : ℝ)⁻¹ *
         (∑ z, ∏ i, if (a i : ZMod (p i)) * (crtExternalPairEquiv p hc z i).1 =
             b i * (crtExternalPairEquiv p hc z i).2 then (1 : ℝ) else 0) =
       ∏ i, (p i : ℝ)⁻¹ := by
   …

   Mentions: OAI.Ostmann.crtExternalPairEquiv