OAI/Geometry/SurfaceImmersion/Whitney/CollarVelocityCalibration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.CollarVelocity.amplitude line 10
2. lemma OAI.ClosedSurfaceR4.CollarVelocity.amplitude_sq line 12
3. theorem OAI.ClosedSurfaceR4.CollarVelocity.calibrated_mean line 17

   Source documentation

   The mean has exactly the prescribed tangential component.

   theorem calibrated_mean {R v a : ℝ} (hR : 0 < R) (hv : 0 < v)
       (hquad : R ^ 2 = v ^ 2 + a ^ 2) :
       circleMean (fun t => density (amplitude R v a) t * arcX (amplitude R v a) t) = v / R := by
   …

   Mentions: OAI.ClosedSurfaceR4.CollarVelocity.circleMean, OAI.ClosedSurfaceR4.CollarVelocity.density, OAI.ClosedSurfaceR4.CollarVelocity.amplitude, OAI.ClosedSurfaceR4.CollarVelocity.arcX

4. lemma OAI.ClosedSurfaceR4.CollarVelocity.circleMean_const_mul line 33
5. theorem OAI.ClosedSurfaceR4.CollarVelocity.calibrated_velocity_means line 40

   Source documentation

   Both weighted velocity means are exact before the positive reparametrization.

   theorem calibrated_velocity_means {R v a : ℝ} (hR : 0 < R) (hv : 0 < v)
       (hquad : R ^ 2 = v ^ 2 + a ^ 2) :
       circleMean (fun t => density (amplitude R v a) t * (R * arcX (amplitude R v a) t)) = v ∧
       circleMean (fun t => density (amplitude R v a) t * (R * arcY (amplitude R v a) t)) = 0 := by
   …

   Mentions: OAI.ClosedSurfaceR4.CollarVelocity.circleMean, OAI.ClosedSurfaceR4.CollarVelocity.density, OAI.ClosedSurfaceR4.CollarVelocity.amplitude, OAI.ClosedSurfaceR4.CollarVelocity.arcX, OAI.ClosedSurfaceR4.CollarVelocity.arcY