OAI/Geometry/SurfaceImmersion/Geometry/PositiveDensityReparam.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Reparametrization converts an exact positive weighted mean into the uniform mean.

  1. def OAI.ClosedSurfaceR4.PositiveDensity.reparametrize line 16
  2. lemma OAI.ClosedSurfaceR4.PositiveDensity.reparametrize_smoothOn line 20
  3. lemma OAI.ClosedSurfaceR4.PositiveDensity.reparametrize_periodic line 30
  4. theorem OAI.ClosedSurfaceR4.PositiveDensity.reparametrize_mean line 42

    Source documentation

    The exact change of variables, for the actual vector-valued velocity.

    theorem reparametrize_mean (hU : IsOpen U) (hρ : ContDiffOn ℝ ∞ ρ (U ×ˢ univ))
    (hpos : ∀ b ∈ U, ∀ t, 0 < ρ (b, t))
    (hper : ∀ b ∈ U, Function.Periodic (fun t => ρ (b, t)) 1)
    (hmass : ∀ b ∈ U, (∫ t in 0..1, ρ (b, t)) = 1)
    (hF : ContDiffOn ℝ ∞ F (U ×ˢ univ)) {b : B} (hb : b ∈ U) :
    (∫ θ in 0..1, reparametrize ρ F (b, θ)) = ∫ t in 0..1, ρ (b, t) • F (b, t) := by
…

    Mentions: OAI.ClosedSurfaceR4.PositiveDensity.reparametrize