LocalStationaryJets.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Local mixed derivative bounds on the actual stationary chart

The chart is smooth on an open pole patch. These lemmas localize the vertical Laplacian estimate to that patch, without extending the chart across its singularities.

theorem OAI.Falconer.iteratedFDeriv_comp_clm_at line 19
theorem OAI.Falconer.directionalLaplacian_contDiffAt line 34
theorem OAI.Falconer.directionalLaplacian_derivative_bound_at line 40
theorem OAI.Falconer.iteratedDirectionalLaplacian_contDiffAt line 56
theorem OAI.Falconer.iteratedDirectionalLaplacian_derivative_bound_at line 65
theorem OAI.Falconer.directionalLaplacian_vertical_at line 84
theorem OAI.Falconer.iteratedDirectionalLaplacian_vertical_on line 115
theorem OAI.Falconer.partialIteratedLaplacian_derivative_bound_on line 136

theorem OAI.Falconer.quadraticJetCoefficient_derivative_bound_on line 155

Source documentation

The actual quadratic coefficient costs exactly 2j additional derivatives, also when differentiated in its external parameters.

theorem quadraticJetCoefficient_derivative_bound_on {n : ℕ} {F : P × Space n → ℂ}
    {U : Set (P × Space n)} (hU : IsOpen U) (hF : ContDiffOn ℝ ∞ F U)
    (j k : ℕ) {p : P} (hp : (p,0) ∈ U) :
    ‖iteratedFDeriv ℝ k (fun q : P => quadraticJetCoefficient j (fun y => F (q,y))) p‖ ≤
      ‖sphereStationaryConstant n / ((2*Complex.I)^j * (j.factorial : ℂ))‖ *
        (n : ℝ)^j * ‖iteratedFDeriv ℝ (k+2*j) F (p,0)‖ := by
…

Mentions: OAI.Falconer.Space, OAI.Falconer.quadraticJetCoefficient, OAI.Falconer.sphereStationaryConstant