PlaneCoefficientTimeJets.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Smooth time dependence of the bounded spatial jets of actual coefficients.

def OAI.ForcedComputation.timePartial line 18

Source documentation

Repeated time differentiation, retaining space as a parameter.

def timePartial : ℕ → (ℝ × Plane → F) → ℝ × Plane → F
  | 0, f => f
  | n+1, f => fun p => fderiv ℝ (timePartial n f) p (1,0)

theorem OAI.ForcedComputation.timePartial_smooth line 22
theorem OAI.ForcedComputation.timePartial_hasDerivAt line 28
theorem OAI.ForcedComputation.timePartial_periodic line 33
theorem OAI.ForcedComputation.timePartial_supported line 43
abbrev OAI.ForcedComputation.CoefficientTimeJets.Jet line 60
def OAI.ForcedComputation.CoefficientTimeJets.extend line 63
Source documentation
Constant continuation is used only to state derivatives within the closed time slab.
```
def extend {T : ℝ} (hT : 0 ≤ T) {k : ℕ} (J : C(Icc (0 : ℝ) T, Jet k))
    (t : ℝ) : Jet k := J (projIcc 0 T hT t)
```
Mentions: OAI.ForcedComputation.CoefficientTimeJets.Jet
theorem OAI.ForcedComputation.CoefficientTimeJets.continuous_extend line 66
theorem OAI.ForcedComputation.CoefficientTimeJets.extend_eq line 70

theorem OAI.ForcedComputation.CoefficientTimeJets.hasDerivWithinAt_extend line 77

Source documentation

The next actual coefficient derivative supplies the derivative of its jet curve.

theorem hasDerivWithinAt_extend {T : ℝ} (hT : 0 ≤ T) {k : ℕ}
    {f : ℝ × Plane → ℝ} (hf : ContDiff ℝ ∞ f) (n : ℕ)
    (J J' : C(Icc (0 : ℝ) T, Jet k))
    (hJ : ∀ t x, BoundedSpatialJets.function Plane ℝ k (J t) x = timePartial n f (t.val,x))
    (hJ' : ∀ t x, BoundedSpatialJets.function Plane ℝ k (J' t) x = timePartial (n+1) f (t.val,x))
    {t : ℝ} (ht : t ∈ Icc (0 : ℝ) T) :
    HasDerivWithinAt (extend hT J) (extend hT J' t) (Icc (0 : ℝ) T) t := by
…

Mentions: OAI.ForcedComputation.CoefficientTimeJets.Jet, OAI.ForcedComputation.BoundedSpatialJets.function, OAI.ForcedComputation.timePartial, OAI.ForcedComputation.CoefficientTimeJets.extend

theorem OAI.ForcedComputation.CoefficientTimeJets.smooth_extend_of_representatives line 97
Source documentation
A continuous hierarchy of actual time derivatives gives all time regularity, at endpoints too.
```
theorem smooth_extend_of_representatives {T : ℝ} (hT : 0 < T) {k : ℕ}
    {f : ℝ × Plane → ℝ} (hf : ContDiff ℝ ∞ f)
    (J : ℕ → C(Icc (0 : ℝ) T, Jet k))
    (hJ : ∀ n t x, BoundedSpatialJets.function Plane ℝ k (J n t) x = timePartial n f (t.val,x))
    (n : ℕ) : ContDiffOn ℝ ∞ (extend hT.le (J n)) (Icc (0 : ℝ) T) := by
…
```
Mentions: OAI.ForcedComputation.CoefficientTimeJets.Jet, OAI.ForcedComputation.BoundedSpatialJets.function, OAI.ForcedComputation.timePartial, OAI.ForcedComputation.CoefficientTimeJets.extend
theorem OAI.ForcedComputation.CoefficientTimeJets.exists_periodic line 121
Source documentation
Smooth periodic scalar coefficients have continuous jets for every time derivative.
```
theorem exists_periodic {T : ℝ} (hT : 0 < T) (k : ℕ)
    {f : ℝ × Plane → ℝ} (hf : ContDiff ℝ ∞ f)
    (hp : ∀ t, PlanePeriodic (fun x => f (t,x))) :
    ∃ J : ℕ → C(Icc (0 : ℝ) T, Jet k),
      (∀ n t x, BoundedSpatialJets.function Plane ℝ k (J n t) x = timePartial n f (t.val,x)) ∧
      (∀ n, ContDiffOn ℝ ∞ (extend hT.le (J n)) (Icc (0 : ℝ) T)) := by
…
```
Mentions: OAI.ForcedComputation.PlanePeriodic, OAI.ForcedComputation.CoefficientTimeJets.Jet, OAI.ForcedComputation.BoundedSpatialJets.function, OAI.ForcedComputation.timePartial, OAI.ForcedComputation.CoefficientTimeJets.extend

theorem OAI.ForcedComputation.CoefficientTimeJets.exists_supported line 133

Source documentation

Common compact spatial support is preserved by every time derivative on the slab.

theorem exists_supported {T : ℝ} (hT : 0 < T) (k : ℕ)
    {f : ℝ × Plane → ℝ} (hf : ContDiff ℝ ∞ f) {K : Set Plane} (hK : IsCompact K)
    (hs : ∀ t ∈ Icc (0 : ℝ) T, ∀ x ∉ K, f (t,x) = 0) :
    ∃ J : ℕ → C(Icc (0 : ℝ) T, Jet k),
      (∀ n t x, BoundedSpatialJets.function Plane ℝ k (J n t) x = timePartial n f (t.val,x)) ∧
      (∀ n, ContDiffOn ℝ ∞ (extend hT.le (J n)) (Icc (0 : ℝ) T)) := by
…

Mentions: OAI.ForcedComputation.CoefficientTimeJets.Jet, OAI.ForcedComputation.BoundedSpatialJets.function, OAI.ForcedComputation.timePartial, OAI.ForcedComputation.CoefficientTimeJets.extend

theorem OAI.ForcedComputation.CoefficientTimeJets.extend_eq_of_representatives line 144
theorem OAI.ForcedComputation.CoefficientTimeJets.periodic_curve_smooth line 155
Source documentation
Smoothness holds for any representative, including the curves in compatible data.
```
theorem periodic_curve_smooth {T : ℝ} (hT : 0 < T) {k : ℕ}
    {f : ℝ × Plane → ℝ} (hf : ContDiff ℝ ∞ f)
    (hp : ∀ t, PlanePeriodic (fun x => f (t,x)))
    (J : C(Icc (0 : ℝ) T, Jet k))
    (hJ : ∀ t x, BoundedSpatialJets.function Plane ℝ k (J t) x = f (t.val,x)) :
    ContDiffOn ℝ ∞ (extend hT.le J) (Icc (0 : ℝ) T) := by
…
```
Mentions: OAI.ForcedComputation.PlanePeriodic, OAI.ForcedComputation.CoefficientTimeJets.Jet, OAI.ForcedComputation.BoundedSpatialJets.function, OAI.ForcedComputation.CoefficientTimeJets.extend
theorem OAI.ForcedComputation.CoefficientTimeJets.supported_curve_smooth line 166