OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternBulkMean.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingPatternBulkMean line 11
2. theorem OAI.Ostmann.movingPatternBulkMean_join line 18
3. theorem OAI.Ostmann.movingPatternInjectionGuard_join line 33
4. theorem OAI.Ostmann.movingPatternBulkMean_guard_average line 48

   Also declared: OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimePatternBulkMean.lean:12 (same declaration text).

5. theorem OAI.Ostmann.movingPattern_original_bulk_mean_eq line 72

   Source documentation

   Averaging only selected bulk coordinates preserves the original signed pattern expression, including the class-injectivity guard.

   theorem movingPattern_original_bulk_mean_eq {A B C : Type*}
       [Fintype A] [Fintype B] [Fintype C] {N n m : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (μ : ℕ → A → ℝ) (ν : B → A → ℝ) (prime : A → ℕ)
       (hmass : ∀ j, ∑ a, ν j a = 1)
       (t : Bool → FrequencyTree ℤ n) (small : Bool → TreeLeafTuple (List B) n)
       (slot : (TreeLeafIndex n × Fin m) ↪ B) (perm : Equiv.Perm (TreeLeafIndex n × Fin m))
       (pattern : Bool × MovingSampleIndex n → C)
       (rep : ∀ c, {i : Bool × MovingSampleIndex n // pattern i = c})
       (G : (Fin (N + 1) → A) → ℂ) (seed : TreeLeafIndex n × Fin m → A) :
       (∑ x, movingOriginalPatternWeight e μ ν prime n pattern G x *
         movingPatternFlagProduct e prime n t small (movingPatternBulkLeaves n m slot perm) pattern rep x) =
       ∑ x, movingOriginalPatternWeight e μ ν prime n pattern (movingPatternBulkMean e ν slot G) x *
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingOriginalPatternWeight, OAI.Ostmann.movingPatternFlagProduct, OAI.Ostmann.movingPatternBulkLeaves, OAI.Ostmann.movingPatternBulkMean

6. theorem OAI.Ostmann.movingPattern_signed_bulk_mean_bound line 94

   Source documentation

   A bound proved for the actual signed bulk mean lifts to the full original pattern law with only its depth-dependent representative-prior cost.

   theorem movingPattern_signed_bulk_mean_bound {A B C : Type*}
       [Fintype A] [Fintype B] [Fintype C] {N n m : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (μ : ℕ → A → ℝ) (ν : B → A → ℝ) (prime : A → ℕ)
       (t : Bool → FrequencyTree ℤ n) (small : Bool → TreeLeafTuple (List B) n)
       (slot : (TreeLeafIndex n × Fin m) ↪ B) (perm : Equiv.Perm (TreeLeafIndex n × Fin m))
       (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)
       (hmass : ∀ j, ∑ a, μ j a = 1) (hnmass : ∀ j, ∑ a, ν j a = 1)
       (hbound : ∀ j a, (prime a : ℝ) * μ j a ≤ E)
       (G : (Fin (N + 1) → A) → ℂ) (D : ℝ) (hD : 0 ≤ D)
       (hG : ∀ x, ‖movingPatternBulkMean e ν slot G x‖ ≤ D)
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingPatternBulkMean