PlaneScalarMildDataFields.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual periodic or compactly supported smooth fields supply all compatible jet data.

theorem OAI.ForcedComputation.PlaneScalarMild.exists_data_of_representatives line 13

theorem OAI.ForcedComputation.PlaneScalarMild.exists_periodic_data line 33

Source documentation

Smooth periodic initial data, source, and coefficients determine compatible finite jets.

theorem exists_periodic_data {T : ℝ} (hT : 0 ≤ T)
    {w₀ : Plane → ℝ} (hw : ContDiff ℝ ∞ w₀) (hpw : PlanePeriodic w₀)
    {h : ℝ × Plane → ℝ} (hh : ContDiff ℝ ∞ h)
    (hph : ∀ t, PlanePeriodic (fun x => h (t,x)))
    {b : Fin 3 → ℝ × Plane → ℝ} (hb : ∀ i, ContDiff ℝ ∞ (b i))
    (hpb : ∀ i t, PlanePeriodic (fun x => b i (t,x))) :
    ∃ D : CompatibleData T,
      (∀ k x, BoundedSpatialJets.function Plane ℝ k (D.initial k) x = w₀ x) ∧
      (∀ k t x, BoundedSpatialJets.function Plane ℝ k (D.source k t) x = h (t.val,x)) ∧
      (∀ k i t x, BoundedSpatialJets.function Plane ℝ k (D.coefficient k i t) x = b i (t.val,x)) := by
…

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

theorem OAI.ForcedComputation.PlaneScalarMild.exists_supported_zero_data line 55

Source documentation

Common compact spatial support gives the whole-plane data, with zero initial value.

theorem exists_supported_zero_data {T : ℝ} {K : Set Plane} (hK : IsCompact K)
    {h : ℝ × Plane → ℝ} (hh : ContDiff ℝ ∞ h)
    (hsh : ∀ t ∈ Icc (0 : ℝ) T, ∀ x ∉ K, h (t,x) = 0)
    {b : Fin 3 → ℝ × Plane → ℝ} (hb : ∀ i, ContDiff ℝ ∞ (b i))
    (hsb : ∀ i t, t ∈ Icc (0 : ℝ) T → ∀ x ∉ K, b i (t,x) = 0) :
    ∃ D : CompatibleData T,
      (∀ k x, BoundedSpatialJets.function Plane ℝ k (D.initial k) x = 0) ∧
      (∀ k t x, BoundedSpatialJets.function Plane ℝ k (D.source k t) x = h (t.val,x)) ∧
      (∀ k i t x, BoundedSpatialJets.function Plane ℝ k (D.coefficient k i t) x = b i (t.val,x)) := by
…

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