AngularJetSymbol.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite-budget angular jets as normalized recursive multipliers

A fixed chart constant is selected before the angular multiplier or its previous derivative order. Taking a jet consumes that exact order from the ambient budget; normalization does not enlarge the derivative scale.

def OAI.Falconer.normalizedAngular line 18
theorem OAI.Falconer.normalizedAngular_restore line 21

theorem OAI.Falconer.ambient_angular_normalization line 28

Source documentation

One fixed normalization controls both ambient and rotated chart jets.

theorem ambient_angular_normalization (n K : ℕ) :
    ∃ H : ℝ, 1 ≤ H ∧ ∀ B : Space (n+2) → ℂ, ContDiff ℝ ∞ B →
      ∀ C D : ℝ, 0 < C → 1 ≤ D →
      (∀ t ≤ K, ∀ w : Sphere (n+2), ‖iteratedFDeriv ℝ t B w‖ ≤ C*D^t) →
      ContDiff ℝ ∞ (normalizedAngular (H*C) B) ∧
      (∀ t ≤ K, ∀ w : Sphere (n+2),
        ‖iteratedFDeriv ℝ t (normalizedAngular (H*C) B) w‖ ≤ D^t) ∧
      ChartSymbolControl K
        (fun (_ : Space (n+2)) (w : Sphere (n+2)) => normalizedAngular (H*C) B w) 1 D := by
…

Mentions: OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.normalizedAngular, OAI.Falconer.ChartSymbolControl

theorem OAI.Falconer.angular_jet_symbol line 89

Source documentation

The initial multiplier needs exactly p+K derivatives for a new order-p jet to remain in the recursive class with K derivatives.

theorem angular_jet_symbol (n K : ℕ) :
    ∃ H : ℝ, 1 ≤ H ∧ ∀ (L : ℕ) (j : MaskJetIndex (n+2))
      (f : Space (n+2) → ℂ), ContDiff ℝ ∞ f → ∀ D : ℝ, 1 ≤ D →
      j.order+K ≤ L →
      (∀ t ≤ L, ∀ w : Sphere (n+2), ‖iteratedFDeriv ℝ t f w‖ ≤ D^t) →
      ContDiff ℝ ∞ (normalizedAngular H (j.scaledValue D⁻¹ f)) ∧
      (∀ t ≤ K, ∀ w : Sphere (n+2),
        ‖iteratedFDeriv ℝ t (normalizedAngular H (j.scaledValue D⁻¹ f)) w‖ ≤ D^t) ∧
      ChartSymbolControl K
        (fun (_ : Space (n+2)) (w : Sphere (n+2)) =>
          normalizedAngular H (j.scaledValue D⁻¹ f) w) 1 D := by
…

Mentions: OAI.Falconer.MaskJetIndex, OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.normalizedAngular, OAI.Falconer.ChartSymbolControl