AmbientMaskProductBudget.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Polynomial mixed-derivative cost of an actual finite mask product

The zeroth-order bound is one. Consequently no constant is raised to the number of descriptors: order k costs only card^k.

theorem OAI.Falconer.ambient_mask_product_derivatives line 19

theorem OAI.Falconer.ambient_mask_product_budget line 59

Source documentation

A fixed positive-order derivative constant is absorbed into each differentiated mask's scale, never into every undifferentiated mask.

theorem ambient_mask_product_budget (S : Finset ι) (f : ι → E → A)
    {C D : ℝ} (hC : 1 ≤ C) (hD : 0 ≤ D) (K : ℕ) (x : E)
    (hf : ∀ i ∈ S, ContDiff ℝ ∞ (f i)) (hzero : ∀ i ∈ S, ‖f i x‖ ≤ 1)
    (hb : ∀ i ∈ S, ∀ k, 1 ≤ k → k ≤ K → ‖iteratedFDeriv ℝ k (f i) x‖ ≤ C*D^k) :
    ∀ k ≤ K, ‖iteratedFDeriv ℝ k (fun z => ∏ i ∈ S, f i z) x‖ ≤ ((S.card : ℝ)*C*D)^k := by
…