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

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

An integrable Gaussian majorant for all spatial shifts in a bounded set.

  1. def OAI.ForcedComputation.PlaneHeat.envelopeCore line 14

    Source documentation

    A slower Gaussian, used to dominate bounded translations of the heat kernel.

    def envelopeCore (t y : ℝ) : ℝ := Real.exp (-((4 * t)⁻¹ / 2) * y ^ 2)
  2. def OAI.ForcedComputation.PlaneHeat.envelopeMoment line 16
  3. def OAI.ForcedComputation.PlaneHeat.shiftCoefficient line 18
  4. theorem OAI.ForcedComputation.PlaneHeat.envelopeCore_pos line 21
  5. theorem OAI.ForcedComputation.PlaneHeat.shiftCoefficient_nonneg line 23
  6. theorem OAI.ForcedComputation.PlaneHeat.shifted_square line 27
  7. theorem OAI.ForcedComputation.PlaneHeat.oneDim_shift_le line 33
  8. theorem OAI.ForcedComputation.PlaneHeat.oneDimDerivative_shift_le line 47
  9. theorem OAI.ForcedComputation.PlaneHeat.envelopeCore_integrable line 60
  10. theorem OAI.ForcedComputation.PlaneHeat.envelopeMoment_integrable line 63
  11. theorem OAI.ForcedComputation.PlaneHeat.functional_norm_le line 74

    Source documentation

    Operator norm of a scalar linear functional in the coordinate maximum norm.

    theorem functional_norm_le (L : Plane →L[ℝ] ℝ) :
    ‖L‖ ≤ |L (Pi.single 0 1)| + |L (Pi.single 1 1)| := by
…
  12. def OAI.ForcedComputation.PlaneHeat.derivativeEnvelope line 95
  13. theorem OAI.ForcedComputation.PlaneHeat.integrable_product line 100
  14. theorem OAI.ForcedComputation.PlaneHeat.derivativeEnvelope_integrable line 105
  15. theorem OAI.ForcedComputation.PlaneHeat.kernel_fderiv_shift_le line 112