OAI/Geometry/SurfaceImmersion/Correction/SurfaceMeanPolynomial.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanTangentExpression line 18
2. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanPolynomial line 22
3. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.coefficientExpressions_smooth line 26
4. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanPolynomial_smooth line 33
5. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanPolynomial_order line 44
6. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanCoefficientValue line 56
7. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanPolynomial_eval line 65

   Source documentation

   Each coefficient used by the slow correction is the mean of the same coefficient in the actual periodic pullback metric.

   lemma meanPolynomial_eval {S : TopologicalSpace.Opens JetPolynomial.Base}
       {G : JetPolynomial.Base → JetPolynomial.Space} (hG : ContDiff ℝ ∞ G)
       (hGO : MapsTo (lowJet G) S O) (n : ℕ) (b c : Bool) (r : Fin n)
       (U : ℕ → Family S Euclidean)
       (hU : ∀ i, VectorExpression.Represents G (l.coefficientExpressions n i) (U i))
       {p : JetPolynomial.Base} (hp : p ∈ S) (t : ℝ) :
       (l.meanPolynomial n b c r).eval G (p,t) =
         meanCoefficientValue (l.geometry G hG hGO) U b c (r.val+1) p := by
   …

   Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanCoefficientValue

8. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanPolynomial_eval_sum line 124

   Source documentation

   The full mean correction is precisely the polynomial perturbation evaluated by the finite-parametrix machinery.

   lemma meanPolynomial_eval_sum {S : TopologicalSpace.Opens JetPolynomial.Base}
       {G : JetPolynomial.Base → JetPolynomial.Space} (hG : ContDiff ℝ ∞ G)
       (hGO : MapsTo (lowJet G) S O) (n : ℕ) (b c : Bool)
       (U : ℕ → Family S Euclidean)
       (hU : ∀ i, VectorExpression.Represents G (l.coefficientExpressions n i) (U i))
       (z : ℝ) {p : JetPolynomial.Base} (hp : p ∈ S) (t : ℝ) :
       Perturbation.eval (l.meanPolynomial n b c) z G (p,t) =
         meanCorrection (l.geometry G hG hGO) U n b c z p := by
   …

   Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanCorrection

9. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanMetric_eq_polynomial line 148

   Source documentation

   The mean pullback metric is the original metric plus the primitive rank-one term and this explicitly constructed polynomial operator.

   theorem meanMetric_eq_polynomial {S : TopologicalSpace.Opens JetPolynomial.Base}
       {G : JetPolynomial.Base → JetPolynomial.Space} (hG : ContDiff ℝ ∞ G)
       (hGO : MapsTo (lowJet G) S O) (n : ℕ) (b c : Bool)
       (U : ℕ → Family S Euclidean)
       (hU : ∀ i, VectorExpression.Represents G (l.coefficientExpressions n i) (U i))
       (z : ℝ) {p : JetPolynomial.Base} (hp : p ∈ S) :
       MetricPolynomial.meanMetric (l.geometry G hG hGO) (coordinateVector 0) U n b c z p =
         inner ℝ
           (fderiv ℝ (fun q => JetVelocityCoordinates.toEuclidean (G q)) p
             (MetricPolynomial.metricDirection (coordinateVector 0) (coordinateVector 1) b))
           (fderiv ℝ (fun q => JetVelocityCoordinates.toEuclidean (G q)) p
             (MetricPolynomial.metricDirection (coordinateVector 0) (coordinateVector 1) c)) +
   …

   Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.q, OAI.ClosedSurfaceR4.JetVelocityCoordinates.toEuclidean

10. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanPolynomial_global_extension line 167

    Source documentation

    Global smooth coefficients for Taylor estimates, retaining exactly the same operator and loss on the compact set of low jets used by the primitive.

    theorem meanPolynomial_global_extension {Q : Set LowJet} (hQ : IsCompact Q)
        (hQO : Q ⊆ O) (n : ℕ) (b c : Bool) :
        ∃ P : Fin n → Expression,
          (∀ r, (P r).SmoothCoeffs univ) ∧
          (∀ r, (P r).order = (l.meanPolynomial n b c r).order) ∧
          (∀ r, (P r).loss = (l.meanPolynomial n b c r).loss) ∧
          ∀ (G : JetPolynomial.Base → JetPolynomial.Space) (z : ℝ)
            (p : JetPolynomial.Base) (t : ℝ), lowJet G p ∈ Q →
            Perturbation.eval P z G (p,t) =
              Perturbation.eval (l.meanPolynomial n b c) z G (p,t) := by
    …

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space