MovingPatternCoefficientMass.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The original pattern coefficients as a finite signed linear functional

theorem OAI.Ostmann.movingOriginalPatternWeight_eq_coefficient_mul line 11

theorem OAI.Ostmann.movingPattern_coefficient_norm_le line 22

Source documentation

Only the internal classes cost a factor of the upper prime cutoff. This bound is used solely for the negligible giant-comparison errors.

theorem movingPattern_coefficient_norm_le {A B C : Type*} [Fintype B] [Fintype C] {N : ℕ}
    (e : Fin (N + 1) ≃ B ⊕ C) (μ : ℕ → A → ℝ) (ν : B → A → ℝ)
    (prime : A → ℕ) (n : ℕ) (pattern : Bool × MovingSampleIndex n → C)
    (rep : ∀ c, {i : Bool × MovingSampleIndex n // pattern i = c})
    (E U : ℝ) (hE : 0 ≤ E) (_hU : 0 ≤ U)
    (hprime : ∀ a, (prime a).Prime) (hμ : ∀ j a, 0 ≤ μ j a) (hν : ∀ j a, 0 ≤ ν j a)
    (hbound : ∀ j a, (prime a : ℝ) * μ j a ≤ E)
    (hsize : ∀ a, (prime a : ℝ) ≤ U) (x : Fin (N + 1) → A) :
    ‖movingOriginalPatternWeight e μ ν prime n pattern (fun _ => 1) x‖ ≤
      (((2 : ℝ) ^ Fintype.card C * E ^ (4 * n * 2 ^ n - Fintype.card C)) * U ^ Fintype.card C) *
        productPrior (fun i => Sum.elim ν (fun c => μ (movingSampleTier (rep c).val.2)) (e i)) x := by
…

Mentions: OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingOriginalPatternWeight, OAI.Ostmann.productPrior, OAI.Ostmann.movingSampleTier

theorem OAI.Ostmann.movingPattern_coefficient_mass_le line 64

theorem OAI.Ostmann.movingPattern_comparison_norm line 89

Source documentation

A uniform giant-comparison error is charged against the original coefficient mass. The ideal signed mean stays inside its norm.

theorem movingPattern_comparison_norm {A B C : Type*}
    [Fintype A] [Fintype B] [Fintype C] {N n : ℕ}
    (e : Fin (N + 1) ≃ B ⊕ C) (μ : ℕ → A → ℝ) (ν : B → A → ℝ)
    (prime : A → ℕ) (pattern : Bool × MovingSampleIndex n → C)
    (rep : ∀ c, {i : Bool × MovingSampleIndex n // pattern i = c})
    (E U ε : ℝ) (hE : 0 ≤ E) (hU : 0 ≤ U) (hε : 0 ≤ ε)
    (hprime : ∀ a, (prime a).Prime) (hμ : ∀ j a, 0 ≤ μ j a) (hν : ∀ j a, 0 ≤ ν j a)
    (hμmass : ∀ j, ∑ a, μ j a = 1) (hνmass : ∀ j, ∑ a, ν j a = 1)
    (hbound : ∀ j a, (prime a : ℝ) * μ j a ≤ E) (hsize : ∀ a, (prime a : ℝ) ≤ U)
    (actual ideal : (Fin (N + 1) → A) → ℂ)
    (hcompare : ∀ x, movingOriginalPatternWeight e μ ν prime n pattern (fun _ => 1) x ≠ 0 →
      ‖actual x - ideal x‖ ≤ ε) :
…

Mentions: OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingOriginalPatternWeight