PlaneScalarMildPointwise.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Scalar interpretation of the effective source and initial value.

def OAI.ForcedComputation.PlaneScalarMild.scalarPathEvaluation line 13
theorem OAI.ForcedComputation.PlaneScalarMild.scalarPathEvaluation_apply line 20
theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solutionJet_function line 26

theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.product_directional_function line 33

Source documentation

The represented derivative of a coefficient product is the actual spatial derivative.

private theorem product_directional_function {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (D : CompatibleData T) (b : Fin 3 → ℝ × Plane → ℝ)
    (hb : ∀ k i t x, BoundedSpatialJets.function Plane ℝ k (D.coefficient k i t) x = b i (t.val,x))
    (k : ℕ) (i : Fin 3) (v : Plane) (t : Icc (0 : ℝ) T) (x : Plane) :
    scalarPathEvaluation k t x (directionalPath k v T
      (productPath (k+1) (D.coefficient (k+1) i) (D.solutionJet hT hν (k+1)))) =
      fderiv ℝ (fun y => b i (t.val,y) * D.solution hT hν t y) x v := by
…

Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData, OAI.ForcedComputation.BoundedSpatialJets.function, OAI.ForcedComputation.PlaneScalarMild.scalarPathEvaluation, OAI.ForcedComputation.PlaneScalarMild.directionalPath, OAI.ForcedComputation.PlaneScalarMild.productPath

theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.effectiveSource_function line 52

Source documentation

The Banach-space effective source has the expected divergence-form scalar value.

theorem effectiveSource_function {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (D : CompatibleData T) (h : ℝ × Plane → ℝ) (b : Fin 3 → ℝ × Plane → ℝ)
    (hh : ∀ k t x, BoundedSpatialJets.function Plane ℝ k (D.source k t) x = h (t.val,x))
    (hb : ∀ k i t x, BoundedSpatialJets.function Plane ℝ k (D.coefficient k i t) x = b i (t.val,x))
    (k : ℕ) (t : Icc (0 : ℝ) T) (x : Plane) :
    BoundedSpatialJets.function Plane ℝ k (D.effectiveSource hT hν k t) x =
      h (t.val,x) + b 0 (t.val,x) * D.solution hT hν t x +
        ∑ j : Fin 2, fderiv ℝ (fun y => b j.succ (t.val,y) * D.solution hT hν t y) x
          (Pi.single j 1) := by
…

Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData, OAI.ForcedComputation.BoundedSpatialJets.function

theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solution_initial line 73
Source documentation
The mild solution takes exactly its prescribed initial value.
```
theorem solution_initial {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (D : CompatibleData T) (x : Plane) :
    D.solution hT hν ⟨0, le_rfl, hT⟩ x = BoundedSpatialJets.function Plane ℝ 0 (D.initial 0) x := by
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData, OAI.ForcedComputation.BoundedSpatialJets.function