OAI/Geometry/SurfaceImmersion/Primitive/WeightedPeriodicPrimitive.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ClosedSurfaceR4.SmoothParameterIntegral.partialIterated_primitive line 19

   Source documentation

   Every slow parameter derivative commutes with the normalized primitive.

   theorem partialIterated_primitive {F : P × ℝ → E} (hF : ContDiff ℝ ∞ F)
       (n : ℕ) (p : P) (x : ℝ) :
       partialIterated n (fun z : P × ℝ => primitive (fun t => F (z.1, t)) z.2) (p, x) =
         primitive (fun t => partialIterated n F (p, t)) x := by
   …

   Mentions: OAI.ClosedSurfaceR4.SmoothParameterIntegral.partialIterated

2. theorem OAI.ClosedSurfaceR4.WeightedEstimates.weighted_rawPrimitive line 54
3. theorem OAI.ClosedSurfaceR4.WeightedEstimates.weighted_periodicPrimitive line 69

   Source documentation

   The normalized primitive has weighted parameter norm at most twice that of its input, uniformly over a fundamental period and at every order.

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

   Mentions: OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound