PolynomialModeConstruction.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Insert the actual tensor-valued polynomial perturbation into the geometric finite correction, using the fixed first-coordinate phase.

abbrev OAI.ClosedSurfaceR4.JetPolynomial.firstPhase line 16
lemma OAI.ClosedSurfaceR4.JetPolynomial.firstPhase_smooth line 18
lemma OAI.ClosedSurfaceR4.JetPolynomial.firstPhase_derivative_bound line 21
def OAI.ClosedSurfaceR4.JetPolynomial.coordinateComplexField line 32
lemma OAI.ClosedSurfaceR4.JetPolynomial.coordinateComplexField_smooth line 35
def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinatePolynomialOperator line 43

theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinatePolynomialOperator_bounds line 54

Source documentation

The constants may depend on the requested norm, whereas tensorLoss P is fixed before the finite correction depth is chosen.

theorem coordinatePolynomialOperator_bounds {Q : Set LowJet}
    (hU : IsOpen U) (hO : IsOpen O) (hQcompact : IsCompact Q) (hQO : Q ⊆ O)
    (P : Fin 3 → Fin n → Expression) (hP : ∀ i l, (P i l).SmoothCoeffs O)
    (K : Compacts Base) (hKU : (K : Set Base) ⊆ U)
    (B : ℕ → ℝ) (hB : ∀ m, 1 ≤ B m) :
    ∃ D : ℕ → ℝ, (∀ m, 0 ≤ D m) ∧ ∀ (G : Base → Space) (hG : ContDiff ℝ ∞ G)
      (hGQ : Set.MapsTo (lowJet G) U Q) (s : ℝ≥0) (τ ε : ℝ),
      0 < τ → 0 < (s : ℝ) → τ ≤ s → s ≤ 1 → 0 ≤ ε → ε ≤ 1 →
      (∀ m, WeightedBound U s (m + tensorOrder P) (B m) (lowJet G)) →
      ∀ m H, supportedWeightedSeminorm
        (K.map planeCoordinateIsometry planeCoordinateIsometry.continuous) s m
        (coordinatePolynomialOperator hO hU P hP hG (fun _ hp => hQO (hGQ hp)) K hKU τ ε H) ≤
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.lowJet, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.tensorOrder, OAI.ClosedSurfaceR4.JetPolynomial.supportedWeightedSeminorm, OAI.ClosedSurfaceR4.JetPolynomial.planeCoordinateIsometry, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinatePolynomialOperator