Strong time differentiation of every actual ordinary L² word, derived from the pointwise evolution and continuous L² spatial jets.

theorem EulerOrdinarySobolev.instOrdinaryWordTime1 : Fact (0 < 1)

noncomputable def EulerOrdinarySobolev.ordinaryWordOperator {n : ℕ} (w : Fin n → Fin 3) : ↥(EulerCylinderSobolevSpace.SobolevSpace 1 n) →L[ℝ] ↥EulerMeanSolenoidal.L2

Ordinary word operator, given by ordinaryLift.toContinuousLinearMap.adjoint.comp (wordOperator 1 ⟨⟨n, Nat.lt_succ_self n⟩,fun i => (w i).succ⟩).

Equations

• One or more equations did not get rendered due to their size.

theorem EulerOrdinarySobolev.ordinaryWordOperator_apply (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {n : ℕ} (w : Fin n → Fin 3) : (ordinaryWordOperator w) (EulerMeanSmoothRepresentative.ordinarySobolev n A.toLp ⋯) = (wordField A w).toLp

noncomputable def EulerOrdinarySobolev.ordinaryWordPath {K : Type u_1} [TopologicalSpace K] (A : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) {n : ℕ} (w : Fin n → Fin 3) : C(K, ↥EulerMeanSolenoidal.L2)

Ordinary word path, given by ⟨fun t => ordinaryWordOperator w (sobolevPath A hA n t), (ordinaryWordOperator w).continuous.comp (sobolevPath A hA n).continuous⟩.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EulerOrdinarySobolev.ordinaryWordPath_apply {K : Type u_1} [TopologicalSpace K] (A : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) {n : ℕ} (w : Fin n → Fin 3) (t : K) : (ordinaryWordPath A hA w) t = (wordField (A t) w).toLp

theorem EulerOrdinarySobolev.wordEnergy_continuous {K : Type u_1} [TopologicalSpace K] (A : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (s : ℕ) : Continuous fun (t : K) => wordEnergy s (A t)

theorem EulerOrdinarySobolev.ordinaryWord_hasDerivWithinAt (T : ℝ) (hT : 0 ≤ T) (A B : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (hB : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (B t).jetLp n) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space), HasDerivAt (fun (r : ℝ) => (A (Set.projIcc 0 T hT r)).field x) ((B ⟨t, ⋯⟩).field x) t) {n : ℕ} (w : Fin n → Fin 3) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (fun (r : ℝ) => (wordField (A (Set.projIcc 0 T hT r)) w).toLp) (wordField (B t) w).toLp (Set.Icc 0 T) ↑t

theorem EulerOrdinarySobolev.wordEnergy_hasDerivWithinAt (T : ℝ) (hT : 0 ≤ T) (A B : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (hB : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (B t).jetLp n) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space), HasDerivAt (fun (r : ℝ) => (A (Set.projIcc 0 T hT r)).field x) ((B ⟨t, ⋯⟩).field x) t) (s : ℕ) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (fun (r : ℝ) => wordEnergy s (A (Set.projIcc 0 T hT r))) (2 * ∑ n ∈ Finset.range (s + 1), ∑ w : Fin n → Fin 3, inner ℝ (wordField (A t) w).toLp (wordField (B t) w).toLp) (Set.Icc 0 T) ↑t