OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/PlanarCutoff.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ForcedComputation.PlanarHamiltonian.rectangleCutoff line 15
2. def OAI.ForcedComputation.PlanarHamiltonian.rectangleCollar line 23
3. def OAI.ForcedComputation.PlanarHamiltonian.rectanglePlateau line 26
4. theorem OAI.ForcedComputation.PlanarHamiltonian.rectangleCutoff_smooth line 29
5. theorem OAI.ForcedComputation.PlanarHamiltonian.rectanglePlateau_open line 34
6. theorem OAI.ForcedComputation.PlanarHamiltonian.mem_rectanglePlateau line 46
7. theorem OAI.ForcedComputation.PlanarHamiltonian.rectangleCutoff_one line 52
8. theorem OAI.ForcedComputation.PlanarHamiltonian.rectangleCutoff_one_near line 65
9. theorem OAI.ForcedComputation.PlanarHamiltonian.rectangleCutoff_support line 70
10. theorem OAI.ForcedComputation.PlanarHamiltonian.rectangleCollar_compact line 95
11. theorem OAI.ForcedComputation.PlanarHamiltonian.rectangleCutoff_compactSupport line 105
12. theorem OAI.ForcedComputation.PlanarHamiltonian.rectangle_field_properties line 114

    Source documentation

    A polynomial Hamiltonian cut off by this explicit collar gives a smooth, compact, divergence-free, mean-zero planar field with the exact local motion.

    theorem rectangle_field_properties {R : RationalBox 2} {δ : ℚ} (hδ : 0 < δ)
        {H : Plane → ℝ} (hH : ContDiff ℝ ∞ H) :
        ContDiff ℝ ∞ (field (fun x => rectangleCutoff R δ x * H x)) ∧
        HasCompactSupport (field (fun x => rectangleCutoff R δ x * H x)) ∧
        (∀ x, divergence (field (fun x => rectangleCutoff R δ x * H x)) x = 0) ∧
        (∫ x, field (fun y => rectangleCutoff R δ y * H y) x) = 0 ∧
        (∀ x ∈ R.carrier, field (fun y => rectangleCutoff R δ y * H y) x = field H x) := by
    …

    Mentions: OAI.ForcedComputation.PlanarHamiltonian.field, OAI.ForcedComputation.PlanarHamiltonian.rectangleCutoff, OAI.ForcedComputation.PlanarHamiltonian.divergence