PlaneScalarMildHeatForm.lean`

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Rewrite the scalar mild equation using one heat operator and the effective source.

def OAI.ForcedComputation.PlaneScalarMild.productPath line 15
Source documentation
A coefficient multiplied by a continuous unknown jet path.
```
def productPath {T : ℝ} (k : ℕ) (b : C(Icc (0 : ℝ) T, Jet k))
    (u : WeaklySingular.Path (Jet k) T) : WeaklySingular.Path (Jet k) T :=
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.WeaklySingular.Path
theorem OAI.ForcedComputation.PlaneScalarMild.productPath_apply line 19
theorem OAI.ForcedComputation.PlaneScalarMild.productPath_truncate line 23
def OAI.ForcedComputation.PlaneScalarMild.kernelSourceOperator line 38
Source documentation
All three raw kernels define bounded source operators on the finite interval.
```
def kernelSourceOperator {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν) (k : ℕ) (i : Fin 3) :
    WeaklySingular.Path (Jet k) T →L[ℝ] WeaklySingular.Path (Jet k) T :=
…
```
Mentions: OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.Jet
theorem OAI.ForcedComputation.PlaneScalarMild.kernelSourceOperator_apply line 44
theorem OAI.ForcedComputation.PlaneScalarMild.kernelSourceOperator_zero line 57
theorem OAI.ForcedComputation.PlaneScalarMild.gradient_integrand_eq_heat line 61
theorem OAI.ForcedComputation.PlaneScalarMild.gradient_integral_eq_heat line 73
theorem OAI.ForcedComputation.PlaneScalarMild.gradientSource_eq_heatSource line 82
Source documentation
A spatial-gradient source operator equals heat applied to the differentiated source.
```
theorem gradientSource_eq_heatSource {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (k : ℕ) (j : Fin 2) (u : WeaklySingular.Path (Jet (k+1)) T) :
    kernelSourceOperator hT hν k j.succ (truncatePath k (k+1) (by omega) T u) =
      heatSourcePath hT hν k (directionalPath k (Pi.single j 1) T u) := by
…
```
Mentions: OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.PlaneScalarMild.kernelSourceOperator, OAI.ForcedComputation.PlaneScalarMild.truncatePath, OAI.ForcedComputation.PlaneScalarMild.heatSourcePath, OAI.ForcedComputation.PlaneScalarMild.directionalPath
theorem OAI.ForcedComputation.PlaneScalarMild.path_sum_apply line 93
theorem OAI.ForcedComputation.PlaneScalarMild.path_add_apply line 100
theorem OAI.ForcedComputation.PlaneScalarMild.linear_source_sum line 104
def OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solutionJet line 113
Source documentation
The unique finite-jet solution used to represent the common scalar function.
```
def solutionJet {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν) (D : CompatibleData T) (k : ℕ) :
    WeaklySingular.Path (Jet k) T :=
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData, OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.Jet
theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solutionJet_truncate line 117
def OAI.ForcedComputation.PlaneScalarMild.CompatibleData.effectiveSource line 125
Source documentation
The true source after moving the drift derivatives off the heat kernel.
```
def effectiveSource {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν) (D : CompatibleData T) (k : ℕ) :
    WeaklySingular.Path (Jet k) T :=
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData, OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.Jet
theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solutionJet_eq_sources line 131
theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.gradientProduct_eq_heatSource line 147
theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solutionJet_heat_form line 164
Source documentation
The common scalar solution satisfies a pure heat Duhamel equation at every jet order.
```
theorem solutionJet_heat_form {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (D : CompatibleData T) (k : ℕ) :
    D.solutionJet hT hν k = initialHeatPath hν k (D.initial (k+1)) +
      heatSourcePath hT hν k (D.effectiveSource hT hν k) := by
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData, OAI.ForcedComputation.PlaneScalarMild.initialHeatPath, OAI.ForcedComputation.PlaneScalarMild.heatSourcePath