OAI/Geometry/SurfaceImmersion/Correction/PolynomialMeanCoefficient.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.JetPolynomial.pairPhases_smooth line 12
2. lemma OAI.ClosedSurfaceR4.JetPolynomial.pairDirections_smooth line 20
3. lemma OAI.ClosedSurfaceR4.JetPolynomial.weighted_starField line 29
4. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.quadraticMeanCoefficient line 46
5. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.quadraticMeanCoefficient_smooth line 50
6. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.quadraticMeanCoefficient_bound line 63

   Source documentation

   This is the actual zero-phase Hessian term, with the fixed polynomial loss, and with the square of the oscillatory amplitude retained.

   theorem quadraticMeanCoefficient_bound {n : ℕ} {U : Set Base} {O Q : Set LowJet}
       (hU : IsOpen U) (hO : IsOpen O) (hQ : IsCompact Q) (hQO : Q ⊆ O)
       (P : Fin n → Expression) (hP : ∀ l, (P l).SmoothCoeffs O)
       (m : ℕ) (B F : ℝ) (hB : 1 ≤ B) (hF : 0 ≤ F) :
       ∃ D : ℝ, 0 ≤ D ∧ ∀ (G : Base → Space) (φ : Base → ℝ)
         (H : Base → Fin 4 → ℂ) (s τ ε C : ℝ),
         0 < τ → 0 < s → τ ≤ s → s ≤ 1 → 0 ≤ ε → ε ≤ 1 → 0 < C →
         ContDiff ℝ ∞ G → ContDiff ℝ ∞ φ → ContDiff ℝ ∞ H →
         Set.MapsTo (lowJet G) U Q → WeightedBound U s (m + order P) B (lowJet G) →
         WeightedBound U s (m + order P) C H →
         (∀ v, WeightedBound U s (m + order P) F (fun p => fderiv ℝ φ p (coordinateVector v))) →
         ∀ t ∈ Set.Icc (0 : ℝ) 1,
   …

   Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.lowJet, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.order, OAI.ClosedSurfaceR4.JetPolynomial.coordinateVector