OAI/Geometry/SurfaceImmersion/Atlas/QuadraticCutoffBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Uniform scale bounds for the local quadratic corrections. The fixed cutoff operator makes the constants independent of the tensor and radius.

  1. abbrev OAI.ClosedSurfaceR4.SphericalJets.SecondTensor line 14
  2. def OAI.ClosedSurfaceR4.SphericalJets.unitJetCutoff line 24
  3. def OAI.ClosedSurfaceR4.SphericalJets.quadraticCutoffOperator line 27
  4. lemma OAI.ClosedSurfaceR4.SphericalJets.quadraticCutoffOperator_apply line 32
  5. lemma OAI.ClosedSurfaceR4.SphericalJets.quadraticCutoffOperator_smooth line 36
  6. lemma OAI.ClosedSurfaceR4.SphericalJets.quadraticCutoffOperator_compact line 48
  7. theorem OAI.ClosedSurfaceR4.SphericalJets.uniform_quadratic_cutoff_bound line 56
  8. def OAI.ClosedSurfaceR4.SphericalJets.scaledQuadraticCutoff line 73
  9. lemma OAI.ClosedSurfaceR4.SphericalJets.scaledQuadraticCutoff_smooth line 76
  10. lemma OAI.ClosedSurfaceR4.SphericalJets.scaledQuadraticCutoff_germ line 81
  11. lemma OAI.ClosedSurfaceR4.SphericalJets.scaledQuadraticCutoff_tsupport line 95
  12. lemma OAI.ClosedSurfaceR4.SphericalJets.scaledQuadraticCutoff_norm_deriv line 107
  13. theorem OAI.ClosedSurfaceR4.SphericalJets.uniform_scaled_quadratic_bounds line 127

    Source documentation

    The three orders have sizes O(r²), O(r), O(1), with one constant for all tensors and all positive radii.

    theorem uniform_scaled_quadratic_bounds : ∃ C : ℝ, 0 ≤ C ∧
    ∀ (B : SecondTensor) (p : Plane) (r : ℝ), 0 < r → ∀ j ≤ 2, ∀ x : Plane,
      r^j * ‖iteratedFDeriv ℝ j (scaledQuadraticCutoff B p r) x‖ ≤ C*‖B‖*r^2 := by
…

    Mentions: OAI.ClosedSurfaceR4.SphericalJets.SecondTensor, OAI.ClosedSurfaceR4.SphericalJets.Plane, OAI.ClosedSurfaceR4.SphericalJets.scaledQuadraticCutoff