MovingPatternExternalPrior.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Original external priors joined to the internal equality-pattern law

Only internal occurrences incur the repetition loss; the bound is uniform in the number of external and protected bulk coordinates.

theorem OAI.Ostmann.movingPattern_external_prior_bound line 16

theorem OAI.Ostmann.movingPattern_fin_prior_bound line 49

Source documentation

The same original-law bound in the exact finite coordinates of the symbolic-line comparison. External coordinates do not enter the loss.

theorem movingPattern_fin_prior_bound {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 : ℝ)
    (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)
    (G : (Fin (N + 1) → A) → ℂ) (D : ℝ) (hD : 0 ≤ D) (hG : ∀ x, ‖G x‖ ≤ D)
    (x : Fin (N + 1) → A) :
    ‖((∏ b, ν b (x (e.symm (.inl b))) : ℝ) : ℂ) *
        (movingPairCompensatedMass μ prime ((movingSamplePairCoordinates A n).symm
          (fun i => x (e.symm (.inr (pattern i))))) : ℂ) * G x‖ *
…

Mentions: OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingPairCompensatedMass, OAI.Ostmann.movingSamplePairCoordinates