MovingPatternSquareError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Prime-square exclusions under the original pattern priors

theorem OAI.Ostmann.movingRepresentativeProduct_error line 13

Source documentation

The relative square error for the actual class-indexed collection of internal primes. Every class has a proved occurrence in the history pair.

theorem movingRepresentativeProduct_error {σ C : Type*} [Fintype C]
    (tier : σ → ℕ) (value : σ → ℕ) (hprime : ∀ i, (value i).Prime)
    (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j)
    {n : ℕ} (T : Bool → MovingSlotData σ n) (hlevels : ∀ b, (T b).Levels tier)
    (rep : C → σ) (base : ∀ c, MovingPairRepresentativeOccurrences T (rep c))
    (hf : ∀ c b, (T b).Frequencies (fun s => (s : ZMod (value (rep c))) ≠ 0))
    (V : ℝ) (hsize : ∀ c, Real.exp V ≤ value (rep c)) :
    letI : ∀ c, Fact (value (rep c)).Prime := fun _ => ⟨hprime _⟩
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingPairRepresentativeOccurrences

theorem OAI.Ostmann.productPrior_relative_error line 60

Source documentation

Integrating a relative local error uses the original normalized prior, not a conditioned law. The retained scale may include every internal class.

theorem productPrior_relative_error {A : Type*} [Fintype A] {N : ℕ}
    (μ : Fin N → A → ℝ) (hmass : ∀ i, ∑ a, μ i a = 1)
    (weight err : (Fin N → A) → ℂ) (scale : (Fin N → A) → ℝ)
    (B K : ℝ) (hK : 0 ≤ K)
    (hweight : ∀ x, ‖weight x‖ * scale x ≤ B * productPrior μ x)
    (herr : ∀ x, weight x ≠ 0 → ‖err x‖ ≤ K * scale x) :
    ‖∑ x, weight x * err x‖ ≤ B * K := by
…

Mentions: OAI.Ostmann.productPrior