NonstationaryPower.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A finite derivative order pays for all graph summations

The polynomial cost of the spatial labels, cap pairs and model masses is included in outer. The derivative order is chosen before R or any cell, cap or endpoint symbol. Constants may depend on that fixed order.

theorem OAI.Falconer.positive_power_gain_order line 15
theorem OAI.Falconer.graph_ibp_arbitrary_power line 36

theorem OAI.Falconer.positive_power_gain_order_ge line 50

Source documentation

The graph order can also cover the derivative budget required by the far step.

theorem positive_power_gain_order_ge {γ : ℝ} (hγ : 0 < γ) (outer T : ℝ)
    (minOrder : ℕ) :
    ∃ m : ℕ, minOrder ≤ m ∧ ∀ {R K q : ℝ}, 1 ≤ R → 0 ≤ K → 0 ≤ q →
      q ≤ K*R^(-γ) → R^outer*q^m ≤ K^m*R^(-T) := by
…