CompactPeriodicAnsatzBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite periodic ansatz bounds with fixed coefficients and a varying fast scale.

lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.compact_lift_derivative_bound line 20
Source documentation
Compact spatial control and periodicity give uniform bounds for all mixed derivatives up to any prescribed finite order.
```
lemma compact_lift_derivative_bound (U : Family A E) {Q : Set A}
    (hQ : IsCompact Q) (m : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ j ≤ m, ∀ p ∈ Q, ∀ t : ℝ,
      ‖iteratedFDeriv ℝ j (fun y : A × ℝ => U.val y.1 (y.2 : Period)) (p,t)‖ ≤ C := by
…
```
Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.Family

lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.compact_fast_derivative_bound line 53

Source documentation

Fast evaluation has precisely the expected derivative-scale loss.

lemma compact_fast_derivative_bound (U : Family A E) {Q : Set A}
    (hQ : IsCompact Q) (ℓ : A →L[ℝ] ℝ) (m : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ z : ℝ, 0 < z → z ≤ 1 → ∀ j ≤ m, ∀ p ∈ Q,
      z^j*‖iteratedFDeriv ℝ j (U.fastValue ℓ z) p‖ ≤ C := by
…

Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.Family

theorem OAI.ClosedSurfaceR4.LocalPeriodicExpansion.compact_finiteAnsatz_bounds line 111

Source documentation

The actual globally smooth finite ansatz has uniform compact-domain jets after multiplication by the corresponding power of the fast scale.

theorem compact_finiteAnsatz_bounds {F : A → E} (hF : ContDiff ℝ ∞ F)
    (U : ℕ → Family O E) {K Q : Set A} (hK : IsClosed K) (hKO : K ⊆ O)
    (hzU : ∀ i p, p ∈ O → p ∉ K → (U i).val p = 0)
    (hQ : IsCompact Q) (ℓ : A →L[ℝ] ℝ) (L : ℕ) :
    ∃ C : ℕ → ℝ, (∀ m, 0 ≤ C m) ∧
      ∀ z : ℝ, 0 < z → z ≤ 1 →
        ContDiff ℝ ∞ (finiteAnsatz F U ℓ L z) ∧
        ∀ m p, p ∈ Q → z^m*‖iteratedFDeriv ℝ m (finiteAnsatz F U ℓ L z) p‖ ≤ C m := by
…

Mentions: OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family, OAI.ClosedSurfaceR4.LocalPeriodicExpansion.finiteAnsatz