PlaneScalarMildData.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Compatible data turn the finite-jet equations into one scalar mild solution.

structure OAI.ForcedComputation.PlaneScalarMild.CompatibleData line 16
Source documentation
Initial data, source, and the three coefficients, represented consistently at every order.
```
structure CompatibleData (T : ℝ) where
…
```

def OAI.ForcedComputation.PlaneScalarMild.CompatibleData.ofRepresentatives line 29

Source documentation

Equality of represented scalar functions supplies compatibility automatically.

def ofRepresentatives {T : ℝ} (w₀ : Plane → ℝ) (h : Icc (0 : ℝ) T → Plane → ℝ)
    (b : Fin 3 → Icc (0 : ℝ) T → Plane → ℝ)
    (J : ∀ k, Jet k) (g : ∀ k, WeaklySingular.Path (Jet k) T)
    (c : ∀ k, Fin 3 → C(Icc (0 : ℝ) T, Jet k))
    (hJ : ∀ k x, BoundedSpatialJets.function Plane ℝ k (J k) x = w₀ x)
    (hg : ∀ k t x, BoundedSpatialJets.function Plane ℝ k (g k t) x = h t x)
    (hc : ∀ k i t x, BoundedSpatialJets.function Plane ℝ k (c k i t) x = b i t x) :
    CompatibleData T where
…

Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.BoundedSpatialJets.function, OAI.ForcedComputation.PlaneScalarMild.CompatibleData

def OAI.ForcedComputation.PlaneScalarMild.CompatibleData.affinePath line 59
Source documentation
The canonical affine term includes the prescribed initial data and actual heat source.
```
def affinePath {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.affinePath_truncate line 63
def OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solution line 79
Source documentation
All finite-order solutions determine this one scalar function.
```
def solution {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.solution_smooth line 83
theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solution_spatial_bound line 89
theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solution_spatial_continuous line 96