OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/BalancedFluid.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The compact balanced application: a machine-only repeated field, a finite initial loader, and the fixed open-cube material observation.

  1. def OAI.ForcedComputation.Balanced.velocity line 14
  2. def OAI.ForcedComputation.Balanced.force line 17
  3. def OAI.ForcedComputation.Balanced.initialLabel line 20
  4. def OAI.ForcedComputation.Balanced.observer line 22
  5. theorem OAI.ForcedComputation.Balanced.force_tail line 24
  6. theorem OAI.ForcedComputation.Balanced.force_tail_periodic line 45
  7. def OAI.ForcedComputation.Balanced.FluidProperties line 55

    Source documentation

    Every clause refers to the named prescribed force and its actual Euclidean Navier--Stokes solution.

    def FluidProperties (I : Alternating.MachineInput) (hI : Alternating.ValidInput I)
    (ν : ℝ) : Prop :=
…

    Mentions: OAI.Alternating.MachineInput, OAI.Alternating.ValidInput

  8. theorem OAI.ForcedComputation.Balanced.fluid_properties line 78