PlaneScalarMildEquation.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Actual finite-jet scalar mild equations with the Gaussian heat and gradient operators.

def OAI.ForcedComputation.PlaneScalarMild.multiplication line 15
Source documentation
Multiplication by a bounded scalar jet, as a bounded linear operator on the unknown jet.
```
def multiplication (k : ℕ) (b : Jet k) : Jet k →L[ℝ] Jet k :=
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet
theorem OAI.ForcedComputation.PlaneScalarMild.multiplication_apply line 19
def OAI.ForcedComputation.PlaneScalarMild.coefficientCurve line 25
Source documentation
A continuous coefficient jet curve induces a continuous curve of multiplication operators.
```
def coefficientCurve {T : ℝ} (k : ℕ) (b : C(Icc (0 : ℝ) T, Jet k)) :
    C(Icc (0 : ℝ) T, Jet k →L[ℝ] Jet k) :=
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet
theorem OAI.ForcedComputation.PlaneScalarMild.coefficientCurve_apply line 32
theorem OAI.ForcedComputation.PlaneScalarMild.integral_sum_eq_raw line 35
theorem OAI.ForcedComputation.PlaneScalarMild.exists_unique_mild line 55
Source documentation
The scalar mild equation is uniquely solvable on every finite time interval in every finite jet order. The three coefficients are div a, -a₀, and -a₁ in the drift equation.
```
theorem exists_unique_mild {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (k : ℕ) (b : Fin 3 → C(Icc (0 : ℝ) T, Jet k))
    (a : WeaklySingular.Path (Jet k) T) :
    ∃! u : WeaklySingular.Path (Jet k) T, ∀ t : Icc (0 : ℝ) T, u t = a t +
      ∑ i, ∫ s in 0..t.val, rawKernels hν k i (t.val-s)
        (multiplication k (b i (projIcc 0 T hT s))
          (WeaklySingular.extendPath (Jet k) hT u s)) := by
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.rawKernels, OAI.ForcedComputation.PlaneScalarMild.multiplication, OAI.ForcedComputation.WeaklySingular.extendPath