WeightedAngularJets.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Uniform spatial estimates after any fixed number of angular derivatives. Angular differentiation does not increase the polynomial scale loss.

def OAI.ClosedSurfaceR4.JetPolynomial.Expression.angles line 16
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_angles line 20
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_angles line 25
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_angles line 30
def OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.angles line 40
def OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.angularFamily line 42
lemma OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.represents_angles line 46

theorem OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.compact_angular_bound line 57

Source documentation

The constant may depend on the derivative orders, but the scale exponent is unchanged by angular or spatial differentiation.

theorem compact_angular_bound {S : TopologicalSpace.Opens Base} {O K : Set LowJet}
    (hO : IsOpen O) (hK : IsCompact K) (hKO : K ⊆ O)
    (R : VectorExpression) (hRs : R.SmoothCoeffs O) (i : Fin 4) (k m : ℕ)
    (B : ℝ) (hB : 1 ≤ B) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (G : Base → Space) (s : ℝ), 0 < s → s ≤ 1 →
      ContDiff ℝ ∞ G → Set.MapsTo (lowJet G) S K →
      WeightedBound S s (m + (R i).order) B (lowJet G) →
      ∀ (U : Family S R4), Represents G R U → ∀ t ∈ Set.Icc (0 : ℝ) 1,
        WeightedBound S s m (D / s ^ (R i).loss)
          (fun p => (angularFamily U k).val p (t : CovarianceCorrector.Period) i) := by
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.lowJet, OAI.ClosedSurfaceR4.JetPolynomial.R4, OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.Represents, OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.angularFamily, OAI.ClosedSurfaceR4.CovarianceCorrector.Period