UniformLinearPerturbedMeanData.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform perturbed mean data in a fixed linear phase chart. Bounds for transporting the polynomial may be chosen independently of the numerical profiles retained by the geometric solver.

theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.uniform_perturbed_mean_transfer_with_chart_profiles line 17

Source documentation

Independent fixed chart bounds control polynomial transport without changing the geometric solver or the profile fitted by its mean data.

theorem uniform_perturbed_mean_transfer_with_chart_profiles {n : ℕ}
    (p₀ : ChartedMeanProfile emptyMetricPolynomial)
    (P : Fin 3 → Fin n → Expression) {O : Set LowJet} (hO : IsOpen O)
    (hP : ∀ k j, (P k j).SmoothCoeffs O) (hQO : p₀.Q ⊆ O)
    (K : Compacts Base) (hKU : (K : Set Base) ⊆ p₀.U)
    (e : OpenPartialHomeomorph SmallModes.Base SmallModes.Base)
    (he : ContDiffOn ℝ ∞ e e.source) (hi : ContDiffOn ℝ ∞ e.symm e.target)
    (hKe : (modeSupport K : Set SmallModes.Base) ⊆ e.source)
    (J I : ℕ → ℝ) (hJ : ∀ m, 1 ≤ J m) (hI : ∀ m, 1 ≤ I m)
    (hebound : ∀ m j, 1 ≤ j → j ≤ m → ∀ x ∈ e.source,
      ‖iteratedFDerivWithin ℝ j e e.source x‖ ≤ J m)
    (hibound : ∀ m j, 1 ≤ j → j ≤ m + 1 → ∀ x ∈ e.target,
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanProfile, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.emptyMetricPolynomial, OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.modeSupport

theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.uniform_linear_perturbed_mean_data_all_profiles line 78

Source documentation

A fixed globally smooth polynomial and linear-phase geometry give one perturbed mean profile before every nearby map and both scales.

theorem uniform_linear_perturbed_mean_data_all_profiles {n : ℕ}
    (P : Fin 3 → Fin n → Expression) (hP : ∀ k j, (P k j).SmoothCoeffs univ)
    {F : Base → Space} (hF : ContDiff ℝ ∞ F)
    {Ω U K : Set SmallModes.Base} (hΩ : IsOpen Ω) (hU : IsOpen U) (hK : IsCompact K)
    (hUK : U ⊆ K) (hKΩ : K ⊆ Ω) {ξ : SmallModes.Base} (hξ : ξ ≠ 0)
    (hImm : ∀ x ∈ Ω, Function.Injective
      (fderiv ℝ (F ∘ planeCoordinateIsometry.symm) x))
    (hgood : ∀ x ∈ Ω, Good (realSecondTensor (F ∘ planeCoordinateIsometry.symm) x) ξ)
    (S : Compacts Base) (hS : (modeSupport S : Set SmallModes.Base) ⊆ U)
    {U₀ : Set Base} (hU₀ : IsOpen U₀) (K₀ : Compacts Base)
    (hU₀K : U₀ ⊆ K₀) (hSU₀ : (S : Set Base) ⊆ U₀)
    {φ : Base → ℝ} (hφ : ContDiff ℝ ∞ φ)
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.modeSupport