OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternGiantSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingPattern_prior_lower line 11
2. theorem OAI.Ostmann.movingPattern_prior_giant_support line 29

   Source documentation

   The original prior supplies all prime-range and frequency-unit conditions for the giant comparison, including the protected bulk coordinates.

   theorem movingPattern_prior_giant_support {A B C I : Type*}
       [Fintype A] [Fintype B] [Fintype C] {N n : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (μ : ℕ → A → ℝ) (ν : B → A → ℝ)
       (prime : A → ℕ) (hinj : Function.Injective prime) (hprime : ∀ a, (prime a).Prime)
       (pattern : Bool × MovingSampleIndex n → C)
       (rep : ∀ c, {i : Bool × MovingSampleIndex n // pattern i = c})
       (tier : A → ℕ) (tierB : B → ℕ)
       (hμtier : ∀ j, j < n → ∀ a, μ j a ≠ 0 → tier a = j)
       (hνtier : ∀ j a, ν j a ≠ 0 → tier a = tierB j) (hB : ∀ b, n ≤ tierB b)
       (S : Finset ℤ) (V lo : ℕ) (t : FrequencyTree (S × S) n)
       (hS : ∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ V) (hVlo : V ≤ lo)
       (hμlo : ∀ j a, μ j a ≠ 0 → lo < prime a)
   …

   Mentions: OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.FrequencyTree

3. theorem OAI.Ostmann.frequencyModel_page_projection line 78

   Source documentation

   Deleting the selected large conductor prime confines the actual Page correction to the history-frequency modulus, including all its powers.

   theorem frequencyModel_page_projection {I : Type*} [Fintype I]
       (S : Finset ℤ) (n V cutoff : ℕ) (t : FrequencyTree (S × S) n)
       (hS : ∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ V) (hcut : V < cutoff)
       (P : Finset ℕ) (p : I → ℕ) (z : Option PrimitiveRealZero)
       (hP : ∀ q ∈ P, q.Prime ∧ cutoff ≤ q) (hp : ∀ i, (p i).Prime ∧ cutoff ≤ p i)
       (hdeleteP : ∀ e, z = some e → ∀ q, deletedConductorPrime e.modulus cutoff = some q → q ∉ P)
       (hdeletep : ∀ e, z = some e → ∀ q, deletedConductorPrime e.modulus cutoff = some q → ∀ i, q ≠ p i) :
       pageAtModulus (∏ b, movingArithmeticModuli (frequencyModelBase S n t ^ (n - 1 + 2))
         p P Finset.univ b) z = pageAtModulus (frequencyModelBase S n t ^ (n - 1 + 2)) z := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.PrimitiveRealZero, OAI.Ostmann.deletedConductorPrime, OAI.Ostmann.pageAtModulus, OAI.Ostmann.movingArithmeticModuli, OAI.Ostmann.frequencyModelBase