PrimitiveSlowIncrement.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Derivative and positional two-jet bounds for the actual slow-map increment. Position coordinates cancel before the two-derivative estimate is applied.

lemma OAI.ClosedSurfaceR4.PrimitiveRealization.lowJet_increment_eq_variation line 14
lemma OAI.ClosedSurfaceR4.PrimitiveRealization.lowJet_increment_position line 23
lemma OAI.ClosedSurfaceR4.PrimitiveRealization.weighted_increment_unscaled line 28
lemma OAI.ClosedSurfaceR4.PrimitiveRealization.slow_increment_C3 line 37
lemma OAI.ClosedSurfaceR4.PrimitiveRealization.slow_increment_lowJet line 47
lemma OAI.ClosedSurfaceR4.PrimitiveRealization.slow_increment_ratio line 67
lemma OAI.ClosedSurfaceR4.PrimitiveRealization.slow_increment_C3_ratio line 71

theorem OAI.ClosedSurfaceR4.PrimitiveRealization.primitive_slow_increment_bounds line 81

Source documentation

The actual update has small C3 displacement and small positional two-jet at every fixed order. The exponents are independent of the order.

theorem primitive_slow_increment_bounds {G : JetPolynomial.Base → JetPolynomial.Space} {W : RealModes.RField 4}
    (hG : ContDiff ℝ ∞ G) (hW : ContDiff ℝ ∞ W)
    {z d b : ℝ} (hz : 0 < z) (hz1 : z ≤ 1) (hb : 0 ≤ b)
    (S : ℕ → ℝ) (hS : ∀ m, 0 ≤ S m)
    (hWb : ∀ m, WeightedBound Set.univ (z ^ b) m
      (S m * z ^ d * z ^ b) W) :
    WeightedBound Set.univ 1 3 (S 3 * z ^ (d - 2 * b))
      ((fun x => G x + W (planeCoordinateIsometry x)) - G) ∧
    (∀ m, WeightedBound Set.univ (z ^ b) m (S (m + 2) * z ^ (d - b))
      (lowJet (fun x => G x + W (planeCoordinateIsometry x)) - lowJet G)) := by
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.RealModes.RField

lemma OAI.ClosedSurfaceR4.PrimitiveRealization.primitive_slow_increment_derivative line 104