OAI/Geometry/SurfaceImmersion/Primitive/LoopDensityPatching.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ClosedSurfaceR4.LoopDensity.patch_densities line 18

   Source documentation

   Nonnegative smooth weights preserve both positivity and the linear moments; normalization gives mass one on the open region where some weight is positive.

   theorem patch_densities
       {p : B → ℝ → Plane} {c : B → Plane}
       (hp : ContDiff ℝ ∞ (fun z : B × ℝ => p z.1 z.2))
       (U : ι → Set B) (hU : ∀ i, IsOpen (U i))
       (ρ : ι → B × ℝ → ℝ)
       (hρ : ∀ i, ContDiffOn ℝ ∞ (ρ i) (U i ×ˢ univ))
       (hpos : ∀ i b, b ∈ U i → ∀ t, 0 < ρ i (b, t))
       (hper : ∀ i b, Function.Periodic (fun t => ρ i (b, t)) 1)
       (hmom : ∀ i b, b ∈ U i →
         (∫ t in 0..1, ρ i (b, t) • augment (p b t)) = augment (c b))
       (ψ : ι → B → ℝ) (hψ : ∀ i, ContDiff ℝ ∞ (ψ i))
       (hn : ∀ i b, 0 ≤ ψ i b) (hsupp : ∀ i, tsupport (ψ i) ⊆ U i) :
   …

   Mentions: OAI.ClosedSurfaceR4.LoopDensity.Plane, OAI.ClosedSurfaceR4.LoopDensity.augment