OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternPriorSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingPattern_coefficient_zero_of_prior line 12

   Source documentation

   Vanishing representative prior forces the original compensated coefficient it dominates to vanish as well.

   theorem movingPattern_coefficient_zero_of_prior {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 : ℝ)
       (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)
       (x : Fin (N + 1) → A)
       (hx : productPrior (fun i => Sum.elim ν
         (fun c => μ (movingSampleTier (rep c).val.2)) (e i)) x = 0) :
       ((∏ b, ν b (x (e.symm (.inl b))) : ℝ) : ℂ) *
         (movingPairCompensatedMass μ prime ((movingSamplePairCoordinates A n).symm
   …

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

2. theorem OAI.Ostmann.movingOriginalPatternWeight_support_restrict line 41

   Source documentation

   Restricting the observable to the representative product support preserves its exact original, compensated pattern weight.

   theorem movingOriginalPatternWeight_support_restrict {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 : ℝ)
       (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) → ℂ) (x : Fin (N + 1) → A) :
       movingOriginalPatternWeight e μ ν prime n pattern
         (fun x => if productPrior (fun i => Sum.elim ν
           (fun c => μ (movingSampleTier (rep c).val.2)) (e i)) x = 0 then 0 else G x) x =
         movingOriginalPatternWeight e μ ν prime n pattern G x := by
   …

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

3. theorem OAI.Ostmann.movingPattern_arithmetic_comparison_on_support line 61