MaskProductBudget.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual buffered masks satisfy finite symbol budgets

Derivative constants depend on dimension and the fixed budget, never on the number of descriptors. Only a polynomial factor in the list size enters positive-order derivatives, and this is absorbed into R^sigma.

theorem OAI.Falconer.buffered_mask_product_bound line 18

theorem OAI.Falconer.descriptor_count_subpower line 64

Source documentation

The list-size loss in the previous theorem is bounded by R^sigma, with no dependence on the angular or spatial data.

theorem descriptor_count_subpower (C : ℕ) {σ : ℝ} (hσ : 0 < σ) :
    ∃ N₀ : ℕ, ∀ N ≥ N₀, ∀ {ι : Type*} (I : Finset ι),
      I.card ≤ (N+1)^C → (I.card : ℝ) ≤ ((2 : ℝ)^N)^σ := by
…