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

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The Gaussian first moment and uniform initial continuity for bounded Lipschitz data.

  1. theorem OAI.ForcedComputation.PlaneHeat.kernel_coordinate_moment line 15
  2. theorem OAI.ForcedComputation.PlaneHeat.kernel_coordinate_integrable line 22
  3. theorem OAI.ForcedComputation.PlaneHeat.kernel_coordinate_integral_le line 27
  4. theorem OAI.ForcedComputation.PlaneHeat.plane_norm_le_coordinate_sum line 40
  5. theorem OAI.ForcedComputation.PlaneHeat.kernel_norm_moment_integrable line 47
  6. theorem OAI.ForcedComputation.PlaneHeat.kernel_norm_moment_le line 57
  7. def OAI.ForcedComputation.PlaneHeat.evolution line 72
  8. theorem OAI.ForcedComputation.PlaneHeat.norm_evolution_sub_le line 75
  9. theorem OAI.ForcedComputation.PlaneHeat.evolution_tendsto_uniformly line 110
  10. theorem OAI.ForcedComputation.PlaneHeat.jet_lipschitz line 126
  11. theorem OAI.ForcedComputation.PlaneHeat.norm_heatOperator_truncate_sub_le line 136
  12. def OAI.ForcedComputation.PlaneHeat.evolutionOperator line 158

    Source documentation

    The heat operator at nonpositive time is the identity. Only strong, applied continuity at zero is asserted; operator-norm continuity there is unnecessary.

    def evolutionOperator (k : ℕ) (t : ℝ) :
    BoundedSpatialJets.Space Plane F k →L[ℝ] BoundedSpatialJets.Space Plane F k :=
…

    Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space

  13. theorem OAI.ForcedComputation.PlaneHeat.evolutionOperator_function line 162
  14. theorem OAI.ForcedComputation.PlaneHeat.evolutionOperator_initial line 173
  15. theorem OAI.ForcedComputation.PlaneHeat.evolutionOperator_truncate_tendsto line 177