FastPhaseBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform weighted bounds after substituting the fast circle phase. Local real lifts keep the constants independent of the number of oscillations.

lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.restrict_open_domain line 17
lemma OAI.ClosedSurfaceR4.WeightedEstimates.weighted_shifted_phase line 25

theorem OAI.ClosedSurfaceR4.JetPolynomial.Expression.compact_periodic_fast_bound line 61

Source documentation

A periodic function represented by an actual jet expression retains its slow-scale loss after evaluation at a fast linear phase.

theorem compact_periodic_fast_bound {S : Set Base} (hS : IsOpen S) {O K : Set LowJet}
    (hO : IsOpen O) (hK : IsCompact K) (hKO : K ⊆ O)
    (e : Expression) (he : e.SmoothCoeffs O)
    (ℓ : Base →L[ℝ] ℝ) (m : ℕ) (B : ℝ) (hB : 1 ≤ B) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (G : Base → Space) (s z : ℝ),
      0 < z → z ≤ s → s ≤ 1 → ContDiff ℝ ∞ G →
      Set.MapsTo (lowJet G) S K →
      WeightedBound S s (m + e.order) B (lowJet G) →
      ∀ (H : Base → Period → ℝ),
        (∀ p ∈ S, ∀ t : ℝ, e.eval G (p, t) = H p (t : Period)) →
        WeightedBound S z m (D / s ^ e.loss)
          (fun p => H p ((ℓ p / z : ℝ) : Period)) := by
…

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

theorem OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.compact_fast_bound line 117

Source documentation

Each actual periodic coefficient has a fast-scale bound with the same slow-scale loss as its jet polynomial.

theorem compact_fast_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)
    (ℓ : Base →L[ℝ] ℝ) (m : ℕ) (B : ℝ) (hB : 1 ≤ B) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (G : Base → Space) (s z : ℝ),
      0 < z → z ≤ 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 →
        WeightedBound S z m (D / s ^ (R i).loss)
          (fun p => U.fastValue ℓ z p 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