PlaneScalarMildSourceRegularity.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Compatibility and spatial regularity of the effective heat source.

theorem OAI.ForcedComputation.PlaneScalarMild.directionalPath_truncate line 13
theorem OAI.ForcedComputation.PlaneScalarMild.map_add_add_sum line 22
theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.product_solution_truncate line 30
theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.directional_product_truncate line 37
theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.effectiveSource_truncate line 48
Source documentation
The effective source represents the same function at every jet order.
```
theorem effectiveSource_truncate {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (D : CompatibleData T) (k n : ℕ) (hkn : k ≤ n) :
    truncatePath k n hkn T (D.effectiveSource hT hν n) = D.effectiveSource hT hν k := by
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData, OAI.ForcedComputation.PlaneScalarMild.truncatePath
def OAI.ForcedComputation.PlaneScalarMild.CompatibleData.effectiveSourceValue line 62
Source documentation
The common scalar effective source.
```
def effectiveSourceValue {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (D : CompatibleData T) (t : Icc (0 : ℝ) T) (x : Plane) : ℝ :=
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData
theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.effectiveSourceValue_eq line 66
theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.effectiveSource_smooth line 80
Source documentation
The effective source has smooth spatial slices, obtained from the compatible finite jets.
```
theorem effectiveSource_smooth {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (D : CompatibleData T) (t : Icc (0 : ℝ) T) :
    ContDiff ℝ ∞ (D.effectiveSourceValue hT hν t) := by
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData
theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.effectiveSource_spatial_continuous line 93
Source documentation
Every spatial derivative of the effective source varies jointly continuously.
```
theorem effectiveSource_spatial_continuous {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (D : CompatibleData T) (k : ℕ) :
    Continuous (fun p : Icc (0 : ℝ) T × Plane =>
      iteratedFDeriv ℝ k (D.effectiveSourceValue hT hν p.1) p.2) := by
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData