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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Spatial derivatives and the time equation of the actual Gaussian source integral.

  1. theorem OAI.ForcedComputation.PlaneScalarMild.heatSourcePath_directional line 14
  2. theorem OAI.ForcedComputation.PlaneScalarMild.function_heatSourcePath line 26
  3. theorem OAI.ForcedComputation.PlaneScalarMild.spatialPartial_heatSourcePath line 43
  4. theorem OAI.ForcedComputation.PlaneScalarMild.spatialPartial_twice_heatSourcePath line 56
  5. def OAI.ForcedComputation.PlaneScalarMild.sourceValue line 69

    Source documentation

    The bounded source is continued constantly in time outside the finite slab.

    def sourceValue {T : ℝ} (hT : 0 ≤ T) (k : ℕ) (q : WeaklySingular.Path (Jet k) T)
    (s : ℝ) (x : Plane) : ℝ :=
…

    Mentions: OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.Jet

  6. def OAI.ForcedComputation.PlaneScalarMild.heatSourceValue line 74

    Source documentation

    Scalar value of the source integral, with the same constant time continuation.

    def heatSourceValue {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν) (k : ℕ)
    (q : WeaklySingular.Path (Jet k) T) (s : ℝ) (x : Plane) : ℝ :=
…

    Mentions: OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.Jet

  7. theorem OAI.ForcedComputation.PlaneScalarMild.sourceValue_directional line 78
  8. theorem OAI.ForcedComputation.PlaneScalarMild.sourceValue_twice_directional line 87
  9. theorem OAI.ForcedComputation.PlaneScalarMild.hasDerivAt_heatSourceValue line 94