OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimePatternSquareError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingPrimePatternSquareDifference line 14
2. theorem OAI.Ostmann.movingPrimePattern_averaged_square_error line 26

   Source documentation

   All square exclusions can be removed under the literal dependent pattern law. The loss keeps the inverse-prime scale from every internal class.

   theorem movingPrimePattern_averaged_square_error {A B C : Type*}
       [Fintype A] [Fintype B] [Fintype C] {N n : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (prime : A → ℕ) (hprime : ∀ a, (prime a).Prime)
       (tierB : B → ℕ) (tierC : C → ℕ) (t : Bool → FrequencyTree ℤ n)
       (small bulk : Bool → TreeLeafTuple (List B) n)
       (pattern : Bool × MovingSampleIndex n → C)
       (rep : ∀ c, {i : Bool × MovingSampleIndex n // pattern i = c})
       (hsmall : ∀ b, ∀ i ∈ flattenMovingSlots n (small b), n ≤ tierB i)
       (hbulk : ∀ b, ∀ i ∈ flattenMovingSlots n (bulk b), n ≤ tierB i)
       (htier : ∀ i, tierC (pattern i) = movingSampleTier i.2)
       (μ : ℕ → A → ℝ) (ν : B → A → ℝ)
       (hμ : ∀ j a, 0 ≤ μ j a) (hν : ∀ j a, 0 ≤ ν j a)
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.movingSampleTier