FactorChartControl.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Admissible chart bounds for the actual separated endpoint factors

The compact constants are chosen for the whole endpoint family before the scale parameters. An order-q operator costs exactly D^q in the symbol size.

theorem OAI.Falconer.SymbolOrder.chartControl line 19

theorem OAI.Falconer.SymbolOrder.chartControlFamily line 64

Source documentation

One constant works for every scale label before a label is fixed.

theorem chartControlFamily {n q : ℕ} {I V : Type*} [MeasurableSpace I]
    [NormedAddCommGroup V] [NormedSpace ℝ V]
    {B : I × Space (n+2) → V → ℂ} {F : I × Space (n+2) → Space (n+2) → ℂ}
    (h : SymbolOrder B F q) (hF : Measurable (Function.uncurry F)) (K : ℕ) :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ (i : I) (C D : ℝ), 0 ≤ C → 1 ≤ D →
      (∀ x k, k ≤ K+q → ∀ z, ‖iteratedFDeriv ℝ k (B (i,x)) z‖ ≤ C*D^k) →
      ChartSymbolControl K (fun x w => F (i,x) w) (A*C*D^q) D := by
…

Mentions: OAI.Falconer.Space, OAI.Falconer.SymbolOrder, OAI.Falconer.ChartSymbolControl