OAI/NumberTheory/Ostmann/Arithmetic/MovingFullPageDeletion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.naturalProduct_coprime_right line 11
2. theorem OAI.Ostmann.MovingSlotData.frequencyProduct_coprime line 20
3. theorem OAI.Ostmann.movingGiantUnitPeriod_coprime line 29
4. theorem OAI.Ostmann.movingFullPairModulus_coprime line 49
5. theorem OAI.Ostmann.movingFullPairModulus_deleted_prime_coprime line 71

   Source documentation

   The deleted large conductor prime cannot divide the full modulus: its remaining prime factors come from the sampled values, spectators and frequencies.

   theorem movingFullPairModulus_deleted_prime_coprime {σ I : Type*}
       (value : σ → ℕ) (hprime : ∀ i, (value i).Prime) (outside : List ℕ)
       (childBound pivotBound : ℕ → ℕ) {n : ℕ} (T : Bool → MovingSlotData σ n)
       (hf : ∀ b, (T b).Frequencies (· ≠ 0)) (q : I → ℕ) (S : Finset I)
       (hq : ∀ i ∈ S, (q i).Prime) (hout : ∀ p ∈ outside, p.Prime)
       (V cutoff : ℕ) (hV : V < cutoff)
       (hfreq : ∀ b, (T b).Frequencies (fun s => s.natAbs ≤ V))
       (r : ℕ) (hr : r.Prime) (hcut : cutoff ≤ r)
       (hvalues : ∀ i, value i ≠ r) (hspec : ∀ i ∈ S, q i ≠ r)
       (houtside : r ∉ outside) :
       r.Coprime (movingFullPairModulus value (fun i => (hprime i).ne_zero) outside
         childBound pivotBound T hf q S) := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingFullPairModulus

6. theorem OAI.Ostmann.movingSplitModulus_page_projection line 118

   Source documentation

   The regular block has no exceptional-character factor after the one prescribed conductor-prime deletion. Its Page weight remains on the reduced block.

   theorem movingSplitModulus_page_projection {σ I : Type*}
       (value : σ → ℕ) (hprime : ∀ i, (value i).Prime) (outside : List ℕ)
       (childBound pivotBound : ℕ → ℕ) {n : ℕ} (T : Bool → MovingSlotData σ n)
       (hf : ∀ b, (T b).Frequencies (· ≠ 0)) (q : I → ℕ) (S : Finset I)
       (hq : ∀ i ∈ S, (q i).Prime) (hout : ∀ p ∈ outside, p.Prime)
       (V cutoff : ℕ) (hV : V < cutoff)
       (hfreq : ∀ b, (T b).Frequencies (fun s => s.natAbs ≤ V))
       (z : Option PrimitiveRealZero)
       (hvalues : ∀ e, z = some e → ∀ r, deletedConductorPrime e.modulus cutoff = some r →
         ∀ i, value i ≠ r)
       (hspec : ∀ e, z = some e → ∀ r, deletedConductorPrime e.modulus cutoff = some r →
         ∀ i ∈ S, q i ≠ r)
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.PrimitiveRealZero, OAI.Ostmann.deletedConductorPrime