OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Scalar/PlaneHeatAppliedContinuity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Joint continuity of heat evolution with a varying bounded initial jet.

  1. theorem OAI.ForcedComputation.PlaneHeat.norm_evolutionOperator_apply_le line 14
  2. def OAI.ForcedComputation.PlaneHeat.appliedHeat line 21
  3. theorem OAI.ForcedComputation.PlaneHeat.appliedHeat_eq line 26
  4. theorem OAI.ForcedComputation.PlaneHeat.norm_appliedHeat_le line 33
  5. theorem OAI.ForcedComputation.PlaneHeat.appliedHeat_time_continuous line 41
  6. theorem OAI.ForcedComputation.PlaneHeat.appliedHeat_joint_continuous line 53

    Source documentation

    The extra first jet supplies uniform initial continuity even when both time and initial data vary.

    theorem appliedHeat_joint_continuous (x : Plane) :
    Continuous (fun p : ℝ × BoundedSpatialJets.Space Plane F 1 => appliedHeat F p.1 x p.2) := by
…

    Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.PlaneHeat.appliedHeat