OAI/Geometry/SurfaceImmersion/Correction/MixedPeriodicMean.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.angleDerivative_sub line 17
2. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.angularIterated_sub line 25
3. def OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.meanLift line 36
4. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.contDiff_meanLift line 38
5. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.angleDerivative_meanLift line 41
6. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.angularIterated_meanLift_succ line 47
7. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.partialIterated_sub line 58
8. theorem OAI.ClosedSurfaceR4.WeightedEstimates.mixed_weighted_mean line 76

   Source documentation

   Averaging does not increase the mixed weighted bound.

   theorem mixed_weighted_mean {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 (meanLift F)) (p, t)‖ ≤ C := by
   …

9. theorem OAI.ClosedSurfaceR4.WeightedEstimates.mixed_weighted_fluctuation line 97

   Source documentation

   Subtracting the mean costs at most a factor of two and no scale loss.

   theorem mixed_weighted_fluctuation {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 (F - meanLift F)) (p, t)‖ ≤ 2 * C := by
   …