OAI/MeasureTheory/Falconer/Estimates/LaplacianBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Quantitative finite-derivative bounds for stationary jets

The Laplacian is a fixed finite sum of second directional derivatives. Expressing that contraction as a continuous linear map gives bounds for all mixed Fréchet derivatives, without replacing them by separate bounds on a single chart coordinate. Vertical unit vectors in a parameter/tangent product give the partial Laplacian used by the actual stationary operators.

  1. def OAI.Falconer.directionalLaplacianTrace line 24
  2. theorem OAI.Falconer.directionalLaplacianTrace_apply line 29
  3. theorem OAI.Falconer.directionalLaplacianTrace_norm_le line 33
  4. def OAI.Falconer.directionalLaplacian line 53
  5. theorem OAI.Falconer.directionalLaplacian_contDiff line 56
  6. theorem OAI.Falconer.directionalLaplacian_derivative_bound line 63
  7. theorem OAI.Falconer.iteratedDirectionalLaplacian_contDiff line 79
  8. theorem OAI.Falconer.iteratedDirectionalLaplacian_derivative_bound line 90

    Source documentation

    Every mixed derivative of order k of the jth directional Laplacian uses only the amplitude's derivative of order k+2j, with loss n^j.

    theorem iteratedDirectionalLaplacian_derivative_bound {n : ℕ} (v : Fin n → E)
    (hv : ∀ i, ‖v i‖ ≤ 1) {f : E → ℂ} (hf : ContDiff ℝ ∞ f) (j k : ℕ) (x : E) :
    ‖iteratedFDeriv ℝ k ((directionalLaplacian v)^[j] f) x‖ ≤
      (n : ℝ)^j * ‖iteratedFDeriv ℝ (k+2*j) f x‖ := by
…

    Mentions: OAI.Falconer.directionalLaplacian

  9. theorem OAI.Falconer.directionalLaplacian_basis line 105
  10. theorem OAI.Falconer.euclidean_iterated_laplacian_derivative_bound line 116
  11. def OAI.Falconer.verticalDirections line 133
  12. theorem OAI.Falconer.verticalDirections_norm line 137
  13. theorem OAI.Falconer.directionalLaplacian_vertical line 141
  14. theorem OAI.Falconer.iteratedDirectionalLaplacian_vertical line 169
  15. theorem OAI.Falconer.partialIteratedLaplacian_derivative_bound line 184

    Source documentation

    The mixed derivative estimate needed for direction-dependent chart jets. The order is exactly k+2j, and the constant is n^j.

    theorem partialIteratedLaplacian_derivative_bound {n : ℕ} {F : P × Space n → ℂ}
    (hF : ContDiff ℝ ∞ F) (j k : ℕ) (z : P × Space n) :
    ‖iteratedFDeriv ℝ k (fun q : P × Space n =>
      ((Laplacian.laplacian : (Space n → ℂ) → (Space n → ℂ))^[j]
        (fun y => F (q.1,y))) q.2) z‖ ≤
      (n : ℝ)^j * ‖iteratedFDeriv ℝ (k+2*j) F z‖ := by
…

    Mentions: OAI.Falconer.Space