OAI/Geometry/SurfaceImmersion/Primitive/MixedPeriodicBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.angularIterated line 16
2. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.contDiff_angularIterated line 20
3. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.angleDerivative_primitive line 28
4. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.angularIterated_primitive_succ line 35
5. theorem OAI.ClosedSurfaceR4.WeightedEstimates.mixed_weighted_primitive line 53

   Source documentation

   Slow derivatives carry the scale weight; angular derivatives do not. The primitive adds no scale loss, uniformly at every mixed derivative order.

   theorem mixed_weighted_primitive {F : P × ℝ → E} (hF : ContDiff ℝ ∞ F)
       {U : Set P} (hU : IsOpen U) {s C : ℝ} (hs : 0 < s) (hC : 0 ≤ C) (m : ℕ)
       (hb : ∀ j k, j + k ≤ m → ∀ p ∈ U, ∀ t ∈ Set.Icc (0 : ℝ) 1,
         s ^ j * ‖partialIterated j (angularIterated k F) (p, t)‖ ≤ C) :
       ∀ j k, j + k ≤ m → ∀ p ∈ U, ∀ t ∈ Set.Icc (0 : ℝ) 1,
         s ^ j * ‖partialIterated j (angularIterated k
           (fun z : P × ℝ => primitive (fun r => F (z.1, r)) z.2)) (p, t)‖ ≤ 2 * C := by
   …