OAI/Geometry/SurfaceImmersion/Primitive/LoopDensityParameter.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.LoopDensity.augment_smooth line 12
2. lemma OAI.ClosedSurfaceR4.LoopDensity.background_smooth line 26
3. lemma OAI.ClosedSurfaceR4.LoopDensity.column_smooth line 30
4. lemma OAI.ClosedSurfaceR4.LoopDensity.momentMap_smooth line 36
5. lemma OAI.ClosedSurfaceR4.LoopDensity.weights_smoothAt line 43
6. lemma OAI.ClosedSurfaceR4.LoopDensity.weights_smoothOn line 50
7. theorem OAI.ClosedSurfaceR4.LoopDensity.exists_positive_density_near line 58

   Source documentation

   Positive weights and an invertible three-moment matrix persist locally; this constructs an actual smooth positive density with the exact required mean.

   theorem exists_positive_density_near
       (hp : ContDiff ℝ ∞ (fun z : B × ℝ => p z.1 z.2)) (hc : ContDiff ℝ ∞ c)
       (hψ : ∀ i, ContDiff ℝ ∞ (ψ i)) (hψnonneg : ∀ i t, 0 ≤ ψ i t)
       (hψper : ∀ i, Function.Periodic (ψ i) 1)
       {b₀ : B} {ε : ℝ} (hε : 0 < ε) (hM : (momentMap (p b₀) ψ).IsInvertible)
       (hw : ∀ i, 0 < weights (p b₀) ψ ε (c b₀) i) :
       ∃ U : Set B, IsOpen U ∧ b₀ ∈ U ∧ ∃ ρ : B × ℝ → ℝ,
         ContDiffOn ℝ ∞ ρ (U ×ˢ Set.univ) ∧
         (∀ b ∈ U, ∀ t, 0 < ρ (b, t)) ∧
         (∀ b, Function.Periodic (fun t => ρ (b, t)) 1) ∧
         ∀ b ∈ U, (∫ t in 0..1, ρ (b, t) • augment (p b t)) = augment (c b) := by
   …

   Mentions: OAI.ClosedSurfaceR4.LoopDensity.momentMap, OAI.ClosedSurfaceR4.LoopDensity.weights, OAI.ClosedSurfaceR4.LoopDensity.augment