OAI/Geometry/SurfaceImmersion/Primitive/PrimitiveTermC1Bounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual primitive tensor terms have a uniform C1 bound from their scalar amplitude and phase-covector coordinate bounds. All constants precede those functions and every later cycle count.

  1. abbrev OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PrimitiveLocalData line 20
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.primitiveLocalPolynomial line 21
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.primitiveLocalPolynomial_smooth line 24
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitive_term_localized line 43
  5. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitive_term_tensor_C1_bound line 66

    Source documentation

    A bound on the actual coordinate amplitude and covector, including one derivative, controls the genuine globally supported primitive term.

    theorem primitive_term_tensor_C1_bound {D : ℝ} (hD : 0 ≤ D) :
    ∃ E : ℝ, 0 ≤ E ∧ ∀ amp phi : M → ℝ,
      ContMDiff planeModel 𝓘(ℝ) ∞ amp → ContMDiff planeModel 𝓘(ℝ) ∞ phi →
      (∀ i p, p ∈ tsupport (B.weight i) →
        |amp p| ≤ D ∧ ‖fderiv ℝ (amp ∘ (chart (i : M)).symm) (chart (i : M) p)‖ ≤ D) →
      (∀ i y, y ∈ (B.chartWeightCompact i : Set JetPolynomial.Base) →
        ‖B.phaseCovectorRead i phi y‖ ≤ D ∧
          ‖fderiv ℝ (B.phaseCovectorRead i phi) y‖ ≤ D) →
      B.TensorWeightedBound 1 1 E (fun p => (amp p)^2 • phaseDifferentialSquare phi p) := by
…

    Mentions: OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseDifferentialSquare

  6. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitive_term_background_C1_bound line 167

    Source documentation

    The same primitive bound is measured in any fixed background atlas.

    theorem primitive_term_background_C1_bound (A : SmoothingAtlas M) {D : ℝ} (hD : 0 ≤ D) :
    ∃ E : ℝ, 0 ≤ E ∧ ∀ amp phi : M → ℝ,
      ContMDiff planeModel 𝓘(ℝ) ∞ amp → ContMDiff planeModel 𝓘(ℝ) ∞ phi →
      (∀ i p, p ∈ tsupport (B.weight i) →
        |amp p| ≤ D ∧ ‖fderiv ℝ (amp ∘ (chart (i : M)).symm) (chart (i : M) p)‖ ≤ D) →
      (∀ i y, y ∈ (B.chartWeightCompact i : Set JetPolynomial.Base) →
        ‖B.phaseCovectorRead i phi y‖ ≤ D ∧
          ‖fderiv ℝ (B.phaseCovectorRead i phi) y‖ ≤ D) →
      A.TensorWeightedBound 1 1 E (fun p => (amp p)^2 • phaseDifferentialSquare phi p) := by
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseDifferentialSquare

  7. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.term_background_C1_bound line 191

    Source documentation

    A single bound works for every term of every family with these actual coordinate amplitude and phase-covector estimates.

    theorem term_background_C1_bound (B A : SmoothingAtlas M) {D : ℝ} (hD : 0 ≤ D) :
    ∃ E : ℝ, 0 ≤ E ∧ ∀ d : SmoothPrimitiveFamily ι u,
      (∀ a i p, p ∈ tsupport (B.weight i) →
        |d.amplitude a p| ≤ D ∧
          ‖fderiv ℝ (d.amplitude a ∘ (chart (i : M)).symm) (chart (i : M) p)‖ ≤ D) →
      (∀ a i y, y ∈ (B.chartWeightCompact i : Set JetPolynomial.Base) →
        ‖B.phaseCovectorRead i (d.phase a) y‖ ≤ D ∧
          ‖fderiv ℝ (B.phaseCovectorRead i (d.phase a)) y‖ ≤ D) →
      ∀ a, A.TensorWeightedBound 1 1 E (d.term a) := by
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart, OAI.ClosedSurfaceR4.JetPolynomial.Base