PlaneScalarMildSmooth.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A common spatially smooth function represented by compatible finite-jet mild solutions.

def OAI.ForcedComputation.PlaneScalarMild.mildSolution line 14
Source documentation
The uniquely determined continuous solution at a fixed finite jet order.
```
def mildSolution {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (k : ℕ) (b : Fin 3 → C(Icc (0 : ℝ) T, Jet k))
    (a : WeaklySingular.Path (Jet k) T) : WeaklySingular.Path (Jet k) T :=
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.WeaklySingular.Path
theorem OAI.ForcedComputation.PlaneScalarMild.mildSolution_spec line 19
theorem OAI.ForcedComputation.PlaneScalarMild.mildSolution_truncate line 28
def OAI.ForcedComputation.PlaneScalarMild.commonFunction line 44
Source documentation
The common scalar function is read from the uniquely determined zeroth-order path.
```
def commonFunction (t : Icc (0 : ℝ) T) (x : Plane) : ℝ :=
…
```
theorem OAI.ForcedComputation.PlaneScalarMild.commonFunction_eq line 53
theorem OAI.ForcedComputation.PlaneScalarMild.commonFunction_smooth line 69
Source documentation
Every finite-order solution represents the same spatially smooth scalar function.
```
theorem commonFunction_smooth (t : Icc (0 : ℝ) T) :
    ContDiff ℝ ∞ (commonFunction hT hν b a t) := by
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.commonFunction
theorem OAI.ForcedComputation.PlaneScalarMild.commonFunction_spatial_bound line 82
Source documentation
On the compact time interval every spatial derivative is uniformly bounded.
```
theorem commonFunction_spatial_bound (k : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ t : Icc (0 : ℝ) T, ∀ x : Plane,
      ‖iteratedFDeriv ℝ k (commonFunction hT hν b a t) x‖ ≤ C := by
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.commonFunction
theorem OAI.ForcedComputation.PlaneScalarMild.commonFunction_spatial_continuous line 98
Source documentation
Every spatial derivative of the common function varies jointly continuously.
```
theorem commonFunction_spatial_continuous (k : ℕ) :
    Continuous (fun p : Icc (0 : ℝ) T × Plane =>
      iteratedFDeriv ℝ k (commonFunction hT hν b a p.1) p.2) := by
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.commonFunction
theorem OAI.ForcedComputation.PlaneScalarMild.commonFunction_continuous line 120
Source documentation
Continuity in time is in the uniform norm, so evaluation is jointly continuous.
```
theorem commonFunction_continuous :
    Continuous (fun p : Icc (0 : ℝ) T × Plane => commonFunction hT hν b a p.1 p.2) := by
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.commonFunction