LinearPhaseTwoJetBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Fixed phase charts transfer original-coordinate prefix bounds to the two-jet profiles needed by the actual mean and quadratic solvers.

theorem OAI.ClosedSurfaceR4.RealModes.realTwoJet_prefix_bound_on line 18
theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.local_realTwoJet_comp_prefix_bound line 60

theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.linear_phase_twoJet_profiles line 96

Source documentation

The profiles work simultaneously at every order, so evaluating the same conclusion at m + 1 supplies the quadratic solver's input profile.

theorem linear_phase_twoJet_profiles {ι : Type*}
    (ξ : ι → SmallModes.Base) (hξ : ∀ i, ξ i ≠ 0)
    (U : ι → Set SmallModes.Base) (hU : ∀ i, IsOpen (U i))
    (K : ι → Compacts SmallModes.Base) (hUK : ∀ i, U i ⊆ K i)
    {U₀ : Set Base} (hU₀ : IsOpen U₀)
    (hinto : ∀ i x, x ∈ U i → planeCoordinateIsometry.symm x ∈ U₀)
    (Pjet : ℕ → ℝ) (hPjet : ∀ m, 0 ≤ Pjet m) :
    ∃ H : ι → ℕ → ℝ, (∀ i m, 1 ≤ H i m) ∧
      ∀ (G : Base → Space), ContDiff ℝ ∞ G → ∀ s : ℝ, 0 < s → s ≤ 1 →
      (∀ m j, j ≤ m + 2 → WeightedBound U₀ 1 j (Pjet m / s ^ (j - 2)) G) →
      ∀ i m, WeightedBound (linearPhaseChart (ξ i) (hξ i) (U i) (hU i)).target
        s m (H i m) (realTwoJet ((G ∘ planeCoordinateIsometry.symm) ∘
…

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