OAI/NumberTheory/Ostmann/Arithmetic/RestoredPrimeCellExpansion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.harmonic_mass_ne_zero_of_sdiff line 13
2. theorem OAI.Ostmann.restored_prime_prior_atom line 22

   Source documentation

   Restoring a prime atom multiplies the full-set normalized prior by exactly the ratio of its harmonic masses, not by a new probability law.

   theorem restored_prime_prior_atom (P S D : Finset ℕ)
       (h : (∑ p ∈ S \ D, (p : ℝ)⁻¹) ≠ 0) (p : P) :
       ((∑ t ∈ S \ D, (t : ℝ)⁻¹)⁻¹ * ∑ t ∈ S, (t : ℝ)⁻¹) * primeSubsetPrior P S p =
         if (p : ℕ) ∈ S then (∑ t ∈ S \ D, (t : ℝ)⁻¹)⁻¹ * (p : ℝ)⁻¹ else 0 := by
   …

   Mentions: OAI.Ostmann.primeSubsetPrior

3. theorem OAI.Ostmann.restored_prime_cell_expansion line 36
4. theorem OAI.Ostmann.restored_bulk_residue_expansion line 77

   Source documentation

   Restored atoms retain both their actual residue labels and the original deleted-set normalizer.

   theorem restored_bulk_residue_expansion {J C : Type*} [Fintype J] [Fintype C]
       (P : Finset ℕ) (M : ℕ) [NeZero M] (u v : J → C → ℝ)
       (c₀ : C × (ZMod M)ˣ)
       (hP : ∀ j, primeCellSupport M (fun c : C × (ZMod M)ˣ => c.2.val.val)
         (fun c => u j c.1) (fun c => v j c.1) ⊆ P)
       (hsep : ∀ j (c d : C × (ZMod M)ˣ), c ≠ d →
         ¬Nat.ModEq M c.2.val.val d.2.val.val ∨ v j c.1 ≤ u j d.1 ∨ v j d.1 ≤ u j c.1)
       (D : J → Finset ℕ)
       (hD : ∀ j, (∑ p ∈ primeCellSupport M (fun c : C × (ZMod M)ˣ => c.2.val.val)
         (fun c => u j c.1) (fun c => v j c.1) \ D j, (p : ℝ)⁻¹) ≠ 0)
       (f : (J → C) → (J → (ZMod M)ˣ) → BulkIntegrand J) :
       let S := fun j => primeCellSupport M (fun c : C × (ZMod M)ˣ => c.2.val.val)
   …

   Mentions: OAI.Ostmann.primeCellSupport, OAI.Ostmann.BulkIntegrand