MovingSamplePatternBudget.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Applying representative-prior domination to the literal sampled pair

def OAI.Ostmann.movingPairCompensatedMass line 10
theorem OAI.Ostmann.movingPairCompensatedMass_pattern line 15

theorem OAI.Ostmann.movingPairCompensatedMass_pattern_bound line 24

Source documentation

The weight bound needed by the proved symbolic-line comparison now applies to the original two sample trees, including each node's u factor.

theorem movingPairCompensatedMass_pattern_bound {A C : Type*} [Fintype C]
    (μ : ℕ → 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)
    (hbound : ∀ j a, (prime a : ℝ) * μ j a ≤ E)
    (G : (C → A) → ℂ) (B : ℝ) (hB : 0 ≤ B) (hG : ∀ x, ‖G x‖ ≤ B) (x : C → A) :
    ‖(movingPairCompensatedMass μ prime
        ((movingSamplePairCoordinates A n).symm (x ∘ pattern)) : ℂ) * G x‖ *
      (∏ c, (prime (x c) : ℝ)⁻¹) ≤
        (B * ((2 : ℝ) ^ Fintype.card C * E ^ (4 * n * 2 ^ n - Fintype.card C))) *
          ∏ c, μ (movingSampleTier (rep c).val.2) (x c) := by
…

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

theorem OAI.Ostmann.sampleEqualityPattern_count_le line 42
theorem OAI.Ostmann.movingSamplePair_pattern_count line 55
Source documentation
A coarse sufficient bound for all patterns at a fixed transfer depth. In particular no bulk-length variable enters the exponent.
```
theorem movingSamplePair_pattern_count (n : ℕ) :
    let _ := sampleSetoidFintype (Bool × MovingSampleIndex n)
…
```
Mentions: OAI.Ostmann.sampleSetoidFintype, OAI.Ostmann.MovingSampleIndex