MaskedJetBudget.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The exact derivative cost of the local stationary coefficients

The actual coefficient of order j costs 2*j derivatives. The fixed patch mask extends it smoothly to the whole ambient space without changing that scale exponent.

theorem OAI.Falconer.actualStationaryCoefficient_uniform_budget line 16
theorem OAI.Falconer.stationaryPatchMask_uniform_budget line 43

theorem OAI.Falconer.maskedStationaryCoefficient_uniform_budget line 64

Source documentation

This global bound is suitable for iterating the inverse recurrence. Only the original symbol's derivatives at sphere points are needed.

theorem maskedStationaryCoefficient_uniform_budget (m j r : ℕ) :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ B : Space (m+3) → ℂ,
      ContDiff ℝ ∞ B → ∀ C D : ℝ, 0 ≤ C → 1 ≤ D →
      (∀ l ≤ r+2*j, ∀ w : Sphere (m+3), ‖iteratedFDeriv ℝ l B w‖ ≤ C*D^l) →
      ∀ k ≤ r, ∀ x : Space (m+3),
        ‖iteratedFDeriv ℝ k (maskedStationaryCoefficient m j B) x‖ ≤ A*C*D^(r+2*j) := by
…

Mentions: OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.maskedStationaryCoefficient

theorem OAI.Falconer.maskedStationaryCoefficient_scaled_budget line 100

Source documentation

A common constant retains each derivative's own scale power. This is the form used by the triangular inverse recursion.

theorem maskedStationaryCoefficient_scaled_budget (m j r : ℕ) :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ B : Space (m+3) → ℂ,
      ContDiff ℝ ∞ B → ∀ C D : ℝ, 0 ≤ C → 1 ≤ D →
      (∀ l ≤ r+2*j, ∀ w : Sphere (m+3), ‖iteratedFDeriv ℝ l B w‖ ≤ C*D^l) →
      ∀ k ≤ r, ∀ x : Space (m+3),
        ‖iteratedFDeriv ℝ k (maskedStationaryCoefficient m j B) x‖ ≤ A*C*D^(k+2*j) := by
…

Mentions: OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.maskedStationaryCoefficient