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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Energy regularity of compact smooth fields, transferred to the Euclidean coordinate convention. Pressure uniqueness is stated modulo time-dependent spatial constants, as in the balanced-box application.

  1. def OAI.ForcedComputation.CompactEuclidean.velocity line 16
  2. theorem OAI.ForcedComputation.CompactEuclidean.velocity_smooth line 19
  3. theorem OAI.ForcedComputation.CompactEuclidean.piField_velocity line 24
  4. theorem OAI.ForcedComputation.CompactEuclidean.velocity_divergence line 29
  5. theorem OAI.ForcedComputation.CompactEuclidean.velocity_support line 38
  6. theorem OAI.ForcedComputation.CompactEuclidean.velocity_energyClass line 47
  7. theorem OAI.ForcedComputation.CompactEuclidean.velocity_global_material_flow line 54
  8. def OAI.ForcedComputation.CompactEuclidean.IsEnergySolutionModuloConstants line 66

    Source documentation

    A pressure class has an energy-regular representative satisfying the equations. Its spatially constant gauge may depend on time.

    def IsEnergySolutionModuloConstants (ν : ℝ) (f u : AlternatingNS.Velocity)
    (p : AlternatingNS.Pressure) : Prop :=
…

    Mentions: OAI.AlternatingNS.Velocity, OAI.AlternatingNS.Pressure

  9. theorem OAI.ForcedComputation.CompactEuclidean.energy_unique_modulo_constants line 72
  10. theorem OAI.ForcedComputation.CompactEuclidean.compact_velocity_solution line 83