OAI/Geometry/SurfaceImmersion/Atlas/WeightedModulatedJets.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Slow-scale bounds on the amplitudes of fast oscillatory jets.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.weighted_complexify line 12
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.weighted_amplitudeDerivative line 24
  3. def OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.jetConstant line 50
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.jetConstant_nonneg line 54
  5. theorem OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.weighted_amplitudeJet line 61

    Source documentation

    Output derivatives remain at the slow scale. Only the length of the jet word contributes short-scale powers.

    theorem weighted_amplitudeJet {U : Set Base} (hU : IsOpen U)
    {φ : Base → ℝ} {Z : Base → ℂ} {τ s C P : ℝ}
    (hτ : 0 < τ) (hs : 0 < s) (hτs : τ ≤ s) (hC : 0 ≤ C) (hP : 0 ≤ P)
    (hφ : ContDiff ℝ ∞ φ) (hZ : ContDiff ℝ ∞ Z) (w : List Base)
    (hw : ∀ v ∈ w, ‖v‖ ≤ 1) (m : ℕ)
    (hb : WeightedBound U s (m + w.length) C Z)
    (hp : ∀ v ∈ w, WeightedBound U s (m + w.length) P (fun p => fderiv ℝ φ p v)) :
    WeightedBound U s m (jetConstant P m w.length * C / τ ^ w.length)
      (amplitudeJet τ φ w Z) := by
…

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.jetConstant, OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.amplitudeJet