HigherJetPolynomial.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite sums of higher-jet monomials retain one scale-loss exponent for every output derivative order, as required in the small-increment step.

theorem OAI.ClosedSurfaceR4.WeightedEstimates.compact_higher_jet_polynomial line 17

Source documentation

The scale loss in a finite higher-jet polynomial is bounded by the largest sum of its additional derivative orders.

theorem compact_higher_jet_polynomial {ι τ : Type*} {U : Set A} {V K : Set J}
    (hU : IsOpen U) (hV : IsOpen V) (hK : IsCompact K) (hKV : K ⊆ V)
    (c : τ → J → E) (hc : ∀ j, ContDiffOn ℝ ∞ (c j) V)
    (b : Finset τ) (a : τ → Finset ι) (vs : τ → ι → List A) (P m : ℕ)
    (hP : ∀ j ∈ b, (∑ i ∈ a j, (vs j i).length) ≤ P) :
    ∃ D : τ → ℝ, (∀ j, 1 ≤ D j) ∧
      ∀ (Q : A → J) (f : τ → ι → A → ℝ) (s B : ℝ) (C : τ → ι → ℝ),
      0 < s → s ≤ 1 → 1 ≤ B → (∀ j ∈ b, ∀ i ∈ a j, 0 ≤ C j i) →
      (∀ j ∈ b, ∀ i ∈ a j, ∀ v ∈ vs j i, ‖v‖ ≤ 1) →
      ContDiffOn ℝ ∞ Q U → Set.MapsTo Q U K → WeightedBound U s m B Q →
      (∀ j ∈ b, ∀ i ∈ a j, ContDiffOn ℝ ∞ (f j i) U) →
      (∀ j ∈ b, ∀ i ∈ a j,
…

Mentions: OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound