OAI/Geometry/SurfaceImmersion/Primitive/LoopDensityLinear.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ClosedSurfaceR4.LoopDensity.Plane line 12
2. abbrev OAI.ClosedSurfaceR4.LoopDensity.Moments line 13
3. def OAI.ClosedSurfaceR4.LoopDensity.augment line 15
4. def OAI.ClosedSurfaceR4.LoopDensity.background line 17
5. def OAI.ClosedSurfaceR4.LoopDensity.column line 19
6. def OAI.ClosedSurfaceR4.LoopDensity.momentMap line 22
7. lemma OAI.ClosedSurfaceR4.LoopDensity.momentMap_apply line 25
8. lemma OAI.ClosedSurfaceR4.LoopDensity.augment_continuous line 29
9. def OAI.ClosedSurfaceR4.LoopDensity.density line 34
10. lemma OAI.ClosedSurfaceR4.LoopDensity.density_pos line 37
11. lemma OAI.ClosedSurfaceR4.LoopDensity.density_periodic line 42
12. lemma OAI.ClosedSurfaceR4.LoopDensity.density_moments line 51
13. def OAI.ClosedSurfaceR4.LoopDensity.weights line 75
14. theorem OAI.ClosedSurfaceR4.LoopDensity.solved_moments line 79

    Source documentation

    Once the moment matrix is invertible, all three equations are solved exactly.

    theorem solved_moments {p : ℝ → Plane} (hp : Continuous p)
        {ψ : Fin 3 → ℝ → ℝ} (hψ : ∀ i, Continuous (ψ i))
        (hM : (momentMap p ψ).IsInvertible) (ε : ℝ) (c : Plane) :
        (∫ t in 0..1, density ε ψ (weights p ψ ε c) t • augment (p t)) = augment c := by
    …

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