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

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

The three genuine heat kernels needed for the scalar mild equation on finite spatial jets.

  1. abbrev OAI.ForcedComputation.PlaneScalarMild.Jet line 14
  2. abbrev OAI.ForcedComputation.PlaneScalarMild.PositiveTime line 15
  3. def OAI.ForcedComputation.PlaneScalarMild.zeroExtension line 17
  4. theorem OAI.ForcedComputation.PlaneScalarMild.zeroExtension_continuous line 20
  5. def OAI.ForcedComputation.PlaneScalarMild.heatCutoff line 30

    Source documentation

    The cutoff is one on the working interval and supplies a global square-root bound.

    def heatCutoff (T : ℝ) (r : PositiveTime) : ℝ :=
…

    Mentions: OAI.ForcedComputation.PlaneScalarMild.PositiveTime

  6. theorem OAI.ForcedComputation.PlaneScalarMild.heatCutoff_continuous line 33
  7. theorem OAI.ForcedComputation.PlaneScalarMild.heatCutoff_nonneg line 38
  8. theorem OAI.ForcedComputation.PlaneScalarMild.heatCutoff_le line 41
  9. theorem OAI.ForcedComputation.PlaneScalarMild.heatCutoff_eq_one line 46
  10. def OAI.ForcedComputation.PlaneScalarMild.scaledTime line 52
  11. theorem OAI.ForcedComputation.PlaneScalarMild.scaledTime_continuous line 55
  12. def OAI.ForcedComputation.PlaneScalarMild.rawHeatKernel line 59

    Source documentation

    The unmodified heat operator, set to zero only at nonpositive times.

    def rawHeatKernel {ν : ℝ} (hν : 0 < ν) (k : ℕ) : ℝ → Jet k →L[ℝ] Jet k :=
…

    Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet

  13. def OAI.ForcedComputation.PlaneScalarMild.heatKernel line 63

    Source documentation

    The globally square-root-bounded heat kernel, unchanged on the working interval.

    def heatKernel {ν : ℝ} (hν : 0 < ν) (k : ℕ) (T : ℝ) : ℝ → Jet k →L[ℝ] Jet k :=
…

    Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet

  14. def OAI.ForcedComputation.PlaneScalarMild.gradientKernel line 68

    Source documentation

    A Cartesian heat derivative needs no additional cutoff.

    def gradientKernel {ν : ℝ} (hν : 0 < ν) (k : ℕ) (j : Fin 2) :
    ℝ → Jet k →L[ℝ] Jet k :=
…

    Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet

  15. theorem OAI.ForcedComputation.PlaneScalarMild.rawHeatKernel_pos line 72
  16. theorem OAI.ForcedComputation.PlaneScalarMild.rawHeatKernel_nonpos line 76
  17. theorem OAI.ForcedComputation.PlaneScalarMild.gradientKernel_pos line 79
  18. theorem OAI.ForcedComputation.PlaneScalarMild.gradientKernel_nonpos line 83
  19. theorem OAI.ForcedComputation.PlaneScalarMild.heatKernel_continuous line 86
  20. theorem OAI.ForcedComputation.PlaneScalarMild.gradientKernel_continuous line 91
  21. theorem OAI.ForcedComputation.PlaneScalarMild.heatKernel_eq_raw line 96
  22. theorem OAI.ForcedComputation.PlaneScalarMild.heatKernel_bound line 103
  23. theorem OAI.ForcedComputation.PlaneScalarMild.gradientKernel_bound line 119
  24. def OAI.ForcedComputation.PlaneScalarMild.kernels line 134

    Source documentation

    Index zero is the heat term; the other two indices are Cartesian derivatives.

    def kernels {ν : ℝ} (hν : 0 < ν) (k : ℕ) (T : ℝ) :
    Fin 3 → ℝ → Jet k →L[ℝ] Jet k :=
…

    Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet

  25. def OAI.ForcedComputation.PlaneScalarMild.rawKernels line 138
  26. def OAI.ForcedComputation.PlaneScalarMild.kernelConstants line 141
  27. theorem OAI.ForcedComputation.PlaneScalarMild.kernelConstants_nonneg line 144
  28. theorem OAI.ForcedComputation.PlaneScalarMild.kernels_continuous line 149
  29. theorem OAI.ForcedComputation.PlaneScalarMild.kernels_bound line 155
  30. theorem OAI.ForcedComputation.PlaneScalarMild.kernels_eq_raw line 161