PlaneScalarMildSource.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The canonical initial-data and source paths for the finite-jet mild equation.

theorem OAI.ForcedComputation.PlaneScalarMild.initialHeat_continuousOn line 15
Source documentation
Strong continuity of heat evolution on any jet with one extra bounded derivative.
```
theorem initialHeat_continuousOn {ν : ℝ} (hν : 0 < ν) (k : ℕ) (J : Jet (k+1)) :
    ContinuousOn (fun t : ℝ => PlaneHeat.evolutionOperator ℝ k (ν*t)
      (BoundedSpatialJets.truncate Plane ℝ k (k+1) (by omega) J)) (Ici 0) := by
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.PlaneHeat.evolutionOperator, OAI.ForcedComputation.BoundedSpatialJets.truncate
def OAI.ForcedComputation.PlaneScalarMild.initialHeatPath line 48
Source documentation
The initial heat evolution as a continuous path, including time zero.
```
def initialHeatPath {T ν : ℝ} (hν : 0 < ν) (k : ℕ) (J : Jet (k+1)) :
    WeaklySingular.Path (Jet k) T :=
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.WeaklySingular.Path
theorem OAI.ForcedComputation.PlaneScalarMild.initialHeatPath_apply line 56
def OAI.ForcedComputation.PlaneScalarMild.heatSourcePath line 62
Source documentation
The artificial positive-time cutoff disappears on the finite integration interval.
```
def heatSourcePath {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν) (k : ℕ)
    (g : WeaklySingular.Path (Jet k) T) : WeaklySingular.Path (Jet k) T :=
…
```
Mentions: OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.Jet
theorem OAI.ForcedComputation.PlaneScalarMild.heatSourcePath_apply line 68
theorem OAI.ForcedComputation.PlaneScalarMild.evolutionOperator_truncate line 82
Source documentation
Heat evolution and truncation commute also at the initial time.
```
theorem evolutionOperator_truncate (k n : ℕ) (hkn : k ≤ n) (r : ℝ) (J : Jet n) :
    BoundedSpatialJets.truncateCLM Plane ℝ k n hkn
      (PlaneHeat.evolutionOperator ℝ n r J) =
      PlaneHeat.evolutionOperator ℝ k r (BoundedSpatialJets.truncateCLM Plane ℝ k n hkn J) := by
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.BoundedSpatialJets.truncateCLM, OAI.ForcedComputation.PlaneHeat.evolutionOperator
theorem OAI.ForcedComputation.PlaneScalarMild.heatSourcePath_truncate line 93
Source documentation
The inhomogeneous source path is compatible with every finite-order truncation.
```
theorem heatSourcePath_truncate {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (k n : ℕ) (hkn : k ≤ n) (g : WeaklySingular.Path (Jet n) T) :
    truncatePath k n hkn T (heatSourcePath hT hν n g) =
      heatSourcePath hT hν k (truncatePath k n hkn T g) := by
…
```
Mentions: OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.PlaneScalarMild.truncatePath, OAI.ForcedComputation.PlaneScalarMild.heatSourcePath
theorem OAI.ForcedComputation.PlaneScalarMild.initialHeatPath_truncate line 105
Source documentation
The initial paths inherit compatibility from their initial jets.
```
theorem initialHeatPath_truncate {T ν : ℝ} (hν : 0 < ν)
    (k n : ℕ) (hkn : k ≤ n) (J : Jet (n+1)) (K : Jet (k+1))
    (hJK : BoundedSpatialJets.truncateCLM Plane ℝ k n hkn
      (BoundedSpatialJets.truncate Plane ℝ n (n+1) (by omega) J) =
      BoundedSpatialJets.truncate Plane ℝ k (k+1) (by omega) K) :
    truncatePath k n hkn T (initialHeatPath hν n J) = initialHeatPath hν k K := by
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.BoundedSpatialJets.truncateCLM, OAI.ForcedComputation.BoundedSpatialJets.truncate, OAI.ForcedComputation.PlaneScalarMild.truncatePath, OAI.ForcedComputation.PlaneScalarMild.initialHeatPath
def OAI.ForcedComputation.PlaneScalarMild.forcingPath line 121
Source documentation
The actual affine forcing path in the scalar variation-of-constants equation.
```
def forcingPath {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν) (k : ℕ)
    (J : Jet (k+1)) (g : WeaklySingular.Path (Jet k) T) :
    WeaklySingular.Path (Jet k) T := initialHeatPath hν k J + heatSourcePath hT hν k g
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.initialHeatPath, OAI.ForcedComputation.PlaneScalarMild.heatSourcePath
theorem OAI.ForcedComputation.PlaneScalarMild.forcingPath_apply line 125

theorem OAI.ForcedComputation.PlaneScalarMild.forcingPath_truncate line 136

Source documentation

Canonical forcing paths retain compatibility at every spatial derivative order.

theorem forcingPath_truncate {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (k n : ℕ) (hkn : k ≤ n) (J : Jet (n+1)) (K : Jet (k+1))
    (hJK : BoundedSpatialJets.truncateCLM Plane ℝ k n hkn
      (BoundedSpatialJets.truncate Plane ℝ n (n+1) (by omega) J) =
      BoundedSpatialJets.truncate Plane ℝ k (k+1) (by omega) K)
    (g : WeaklySingular.Path (Jet n) T) :
    truncatePath k n hkn T (forcingPath hT hν n J g) =
      forcingPath hT hν k K (truncatePath k n hkn T g) := by
…

Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.BoundedSpatialJets.truncateCLM, OAI.ForcedComputation.BoundedSpatialJets.truncate, OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.truncatePath, OAI.ForcedComputation.PlaneScalarMild.forcingPath