UniformLinearPhaseBudgets.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Fixed numerical mean budgets for nearby immersions in a linear phase chart. The chart, cut-off, coefficient form, and weighted two-jet profile are fixed before the nearby immersion and slow scale are supplied.

structure OAI.ClosedSurfaceR4.PhaseMean.BudgetProfiles line 17
Source documentation
The numerical part of the local mean budgets, without the map or scale.
```
structure BudgetProfiles where
…
```
def OAI.ClosedSurfaceR4.PhaseMean.Budgets.profiles line 33

theorem OAI.ClosedSurfaceR4.PhaseGeometry.uniform_linear_phase_budgets_all_profiles line 59

Source documentation

All seven mean-budget profiles can be chosen before a nearby immersion and its actual slow scale. The dependence on its two-jet is the displayed fixed profile H, rather than an implicit map-dependent constant.

theorem uniform_linear_phase_budgets_all_profiles {F : RField 4} (hF : ContDiff ℝ ∞ F)
    {Ω U K : Set Base} (hΩ : IsOpen Ω) (hU : IsOpen U) (hK : IsCompact K)
    (hUK : U ⊆ K) (hKΩ : K ⊆ Ω) {ξ : Base} (hξ : ξ ≠ 0)
    (hImm : ∀ x ∈ Ω, Function.Injective (fderiv ℝ F x))
    (hgood : ∀ x ∈ Ω, Good (realSecondTensor F x) ξ)
    {ψ : Base → ℝ} (hψ : ContDiff ℝ ∞ ψ) (Q : PhaseMean.Tensor →L[ℝ] ℝ)
    : ∃ ρ : ℝ, 0 < ρ ∧ ∀ (H : ℕ → ℝ), (∀ m, 1 ≤ H m) →
    ∃ b : BudgetProfiles,
      ∀ (G : RField 4), ContDiff ℝ ∞ G → ∀ C₀ : ℝ, 0 ≤ C₀ → C₀ < ρ →
      WeightedBound univ 1 2 C₀ (G-F) →
      ∀ s : ℝ, 0 < s → s ≤ 1 →
      (∀ m, WeightedBound (linearPhaseChart ξ hξ U hU).target s m (H m)
…

Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.Good, OAI.ClosedSurfaceR4.PhaseMean.Tensor, OAI.ClosedSurfaceR4.PhaseGeometry.linearPhaseChart

theorem OAI.ClosedSurfaceR4.PhaseGeometry.uniform_linear_phase_budgets line 175

Source documentation

theorem uniform_linear_phase_budgets {F : RField 4} (hF : ContDiff ℝ ∞ F)
    {Ω U K : Set Base} (hΩ : IsOpen Ω) (hU : IsOpen U) (hK : IsCompact K)
    (hUK : U ⊆ K) (hKΩ : K ⊆ Ω) {ξ : Base} (hξ : ξ ≠ 0)
    (hImm : ∀ x ∈ Ω, Function.Injective (fderiv ℝ F x))
    (hgood : ∀ x ∈ Ω, Good (realSecondTensor F x) ξ)
    {ψ : Base → ℝ} (hψ : ContDiff ℝ ∞ ψ) (Q : PhaseMean.Tensor →L[ℝ] ℝ)
    (H : ℕ → ℝ) (hH : ∀ m, 1 ≤ H m) :
    ∃ (ρ : ℝ) (b : BudgetProfiles), 0 < ρ ∧
      ∀ (G : RField 4), ContDiff ℝ ∞ G → ∀ C₀ : ℝ, 0 ≤ C₀ → C₀ < ρ →
      WeightedBound univ 1 2 C₀ (G-F) →
      ∀ s : ℝ, 0 < s → s ≤ 1 →
      (∀ m, WeightedBound (linearPhaseChart ξ hξ U hU).target s m (H m)
…

Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.Good, OAI.ClosedSurfaceR4.PhaseMean.Tensor, OAI.ClosedSurfaceR4.PhaseGeometry.linearPhaseChart