OAI/Geometry/SurfaceImmersion/Primitive/LoopDensityBumpSelection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Replace three nondegenerate point masses by smooth positive-density data.

  1. abbrev OAI.ClosedSurfaceR4.LoopDensity.Columns line 13
  2. def OAI.ClosedSurfaceR4.LoopDensity.columnOperator line 15
  3. lemma OAI.ClosedSurfaceR4.LoopDensity.columnOperator_smooth line 18
  4. lemma OAI.ClosedSurfaceR4.LoopDensity.momentMap_eq_columnOperator line 23
  5. theorem OAI.ClosedSurfaceR4.LoopDensity.select_positive_moment_bumps line 28

    Source documentation

    A strictly positive, nondegenerate three-point barycenter can be replaced by smooth nonnegative periodic bumps and a strictly positive constant density.

    theorem select_positive_moment_bumps {p : ℝ → Plane} (hp : Continuous p)
    {t : Fin 3 → ℝ} (ht : ∀ i, t i ∈ Ioo (0 : ℝ) 1)
    {c : Plane} {w : Moments}
    (hM : (columnOperator (fun i => augment (p (t i)))).IsInvertible)
    (hw : ∀ i, 0 < w i)
    (hbary : columnOperator (fun i => augment (p (t i))) w = augment c) :
    ∃ ψ : Fin 3 → ℝ → ℝ, (∀ i, ContDiff ℝ ∞ (ψ i)) ∧
      (∀ i, Function.Periodic (ψ i) 1) ∧ (∀ i x, 0 ≤ ψ i x) ∧
      (∀ i, (∫ x in 0..1, ψ i x) = 1) ∧
      ∃ ε : ℝ, 0 < ε ∧ (momentMap p ψ).IsInvertible ∧
        ∀ i, 0 < weights p ψ ε c i := by
…

    Mentions: OAI.ClosedSurfaceR4.LoopDensity.Plane, OAI.ClosedSurfaceR4.LoopDensity.Moments, OAI.ClosedSurfaceR4.LoopDensity.columnOperator, OAI.ClosedSurfaceR4.LoopDensity.augment, OAI.ClosedSurfaceR4.LoopDensity.momentMap, OAI.ClosedSurfaceR4.LoopDensity.weights