InverseAngularSymbol.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual inverse coefficients preserve the finite angular symbol budget

The geometric coefficient and the newly differentiated multiplier are normalized by one constant chosen before all descriptor lists and scales. The derivative scale stays fixed; only the consumed order is removed.

theorem OAI.Falconer.inverse_seed_coefficient_budget line 20

Source documentation

Simultaneous bounds for all required derivatives of every geometric coefficient, independent of the descriptor labels and initial orders.

theorem inverse_seed_coefficient_budget (m j K : ℕ) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ (ι : Type) [Fintype ι] [DecidableEq ι],
      ∀ (k : ι → MaskJetIndex (m+3))
        (a : ((MaskJetExpansion.seed k).inverse m j).index),
      ∀ t ≤ K, ∀ w : Sphere (m+3),
        ‖iteratedFDeriv ℝ t (((MaskJetExpansion.seed k).inverse m j).term a).coefficient w‖ ≤ C := by
…

Mentions: OAI.Falconer.MaskJetIndex, OAI.Falconer.MaskJetExpansion.seed, OAI.Falconer.Sphere

theorem OAI.Falconer.inverse_angular_symbol line 42

Source documentation

This is the angular multiplier appearing in an actual separated inverse term. Taking order p requires exactly p+K derivatives of the old multiplier.

theorem inverse_angular_symbol (m j K : ℕ) :
    ∃ A : ℝ, 1 ≤ A ∧ ∀ (ι : Type) [Fintype ι] [DecidableEq ι],
      ∀ (k : ι → MaskJetIndex (m+3))
        (a : ((MaskJetExpansion.seed k).inverse m j).index)
        (p : MaskJetIndex (m+3)) (L : ℕ) (f : Space (m+3) → ℂ),
      ContDiff ℝ ∞ f → ∀ D : ℝ, 1 ≤ D → p.order+K ≤ L →
      (∀ t ≤ L, ∀ w : Sphere (m+3), ‖iteratedFDeriv ℝ t f w‖ ≤ D^t) →
      let g := fun z => (((MaskJetExpansion.seed k).inverse m j).term a).coefficient z *
…

Mentions: OAI.Falconer.MaskJetIndex, OAI.Falconer.MaskJetExpansion.seed, OAI.Falconer.Space, OAI.Falconer.Sphere