OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/CompactDetectorScalarTranslation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Spatial translation of the scalar equation and its torus mass. The center is an arbitrary real point; no rationality restriction is imposed.

  1. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.spatialD_translated line 13
  2. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.scalarLaplacian_translated line 18
  3. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.scalarGenerator_translated line 27
  4. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.scalar_solution_translated line 33
  5. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.global_scalar_solution_translated line 53
  6. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.integral_translated line 62

    Source documentation

    Translation preserves the integral over the torus. The proof uses the zero integral of each periodic derivative along the translation path.

    theorem integral_translated {f : Plane → ℝ} (hf : ContDiff ℝ ∞ f)
    (hp : PlanePeriodic f) (δ : Plane) :
    (∫ x in Icc (0 : Plane) (fun _ => 1), f (x + δ)) =
      ∫ x in Icc (0 : Plane) (fun _ => 1), f x := by
…

    Mentions: OAI.ForcedComputation.PlanePeriodic

  7. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.scalarMass_translated line 102