Time derivative of ∫ ∂_iT ∂_jT

Source: enhance.tex 8780–8800. For a divergence-free smooth periodic drift b, the drift terms of D_t ∇T = ∂_t ∇T + b·∇∇T cancel in ∫ (D_t∂_iT ∂_jT + ∂_iT D_t∂_jT), since they integrate to ∫ b·∇(∂_iT ∂_jT) = -∫ (∇·b) ∂_iT ∂_jT = 0. We also build the continuous extension matGradExt of D_t ∇T to the closed half-space t ≥ 0.

def AVenhance.Infra.Section5.LeftToShow.halfSpace : Set (ℝ × Homogenization.Vec 2)

The closed half-space t ≥ 0.

Equations

• AVenhance.Infra.Section5.LeftToShow.halfSpace = Set.Ici 0 ×ˢ Set.univ

noncomputable def AVenhance.Infra.Section5.LeftToShow.gradCoord (T : ℝ → Homogenization.Vec 2 → ℝ) (i : Fin 2) (p : ℝ × Homogenization.Vec 2) : ℝ

The i-th spatial gradient component as a function on space-time.

Equations

• AVenhance.Infra.Section5.LeftToShow.gradCoord T i p = AVenhance.spaceGrad (T p.1) p.2 i

theorem AVenhance.Infra.Section5.LeftToShow.uniqueDiffOn_halfSpace : UniqueDiffOn ℝ halfSpace

theorem AVenhance.Infra.Section5.LeftToShow.isOpen_posSpace : IsOpen (Set.Ioi 0 ×ˢ Set.univ)

theorem AVenhance.Infra.Section5.LeftToShow.posSpace_subset_halfSpace : Set.Ioi 0 ×ˢ Set.univ ⊆ halfSpace

theorem AVenhance.Infra.Section5.LeftToShow.halfSpace_mem_nhds {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : halfSpace ∈ nhds (t, x)

theorem AVenhance.Infra.Section5.LeftToShow.gradCoord_contDiffOn {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) halfSpace) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (gradCoord T i) halfSpace

theorem AVenhance.Infra.Section5.LeftToShow.gradCoord_slice_contDiff {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) halfSpace) (i : Fin 2) {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => gradCoord T i (t, y)

theorem AVenhance.Infra.Section5.LeftToShow.differentiableAt_gradCoord {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) halfSpace) (i : Fin 2) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : DifferentiableAt ℝ (gradCoord T i) (t, x)

theorem AVenhance.Infra.Section5.LeftToShow.hasDerivAt_gradCoord_time {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) halfSpace) (i : Fin 2) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : HasDerivAt (fun (r : ℝ) => gradCoord T i (r, x)) ((fderiv ℝ (gradCoord T i) (t, x)) (1, 0)) t

theorem AVenhance.Infra.Section5.LeftToShow.fderiv_spatial_eq {G : ℝ × Homogenization.Vec 2 → ℝ} {t : ℝ} {x : Homogenization.Vec 2} (hG : DifferentiableAt ℝ G (t, x)) (v : Homogenization.Vec 2) : (fderiv ℝ G (t, x)) (0, v) = (fderiv ℝ (fun (y : Homogenization.Vec 2) => G (t, y)) x) v

Restricting a space-time derivative to a spatial direction.

theorem AVenhance.Infra.Section5.LeftToShow.materialGrad_apply_eq {T : ℝ → Homogenization.Vec 2 → ℝ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) halfSpace) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) (i : Fin 2) : materialGrad b T t x i = (fderiv ℝ (gradCoord T i) (t, x)) (1, 0) + (fderiv ℝ (fun (y : Homogenization.Vec 2) => gradCoord T i (t, y)) x) (b t x)

At positive times the material gradient is the time derivative plus the advective term.

noncomputable def AVenhance.Infra.Section5.LeftToShow.matGradExt (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (T : ℝ → Homogenization.Vec 2 → ℝ) (i : Fin 2) (p : ℝ × Homogenization.Vec 2) : ℝ

The continuous extension of D_t ∇T to t ≥ 0.

Equations

• AVenhance.Infra.Section5.LeftToShow.matGradExt b T i p = (fderivWithin ℝ (AVenhance.Infra.Section5.LeftToShow.gradCoord T i) AVenhance.Infra.Section5.LeftToShow.halfSpace p) (1, b p.1 p.2)

theorem AVenhance.Infra.Section5.LeftToShow.matGradExt_eq_materialGrad {T : ℝ → Homogenization.Vec 2 → ℝ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) (i : Fin 2) : matGradExt b T i (t, x) = materialGrad b T t x i

theorem AVenhance.Infra.Section5.LeftToShow.matGradExt_continuousOn {T : ℝ → Homogenization.Vec 2 → ℝ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) halfSpace) (i : Fin 2) : ContinuousOn (matGradExt b T i) halfSpace

theorem AVenhance.Infra.Section5.LeftToShow.clm_apply_eq_vecDot (L : Homogenization.Vec 2 →L[ℝ] ℝ) (v : Homogenization.Vec 2) : L v = Homogenization.vecDot v fun (k : Fin 2) => L (Homogenization.basisVec k)

A linear functional evaluated on a vector is the dot product with its values on the basis.

theorem AVenhance.Infra.Section5.LeftToShow.spatialDivergence_eq_sum {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) (t : ℝ) (x : Homogenization.Vec 2) : Flow.spatialDivergence b t x = ∑ k : Fin 2, spaceGrad (fun (y : Homogenization.Vec 2) => b t y k) x k

∇·b as the sum of coordinate derivatives of the slice.

theorem AVenhance.Infra.Section5.LeftToShow.continuous_slice_drift {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) (t : ℝ) : Continuous (b t)

noncomputable def AVenhance.Infra.Section5.LeftToShow.driftTerm (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (i j : Fin 2) (x : Homogenization.Vec 2) : ℝ

The advective term b·∇(∂_iT ∂_jT).

Equations

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

theorem AVenhance.Infra.Section5.LeftToShow.fderiv_mul_add_eq_driftTerm {T : ℝ → Homogenization.Vec 2 → ℝ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) halfSpace) {t : ℝ} (ht : 0 ≤ t) (i j : Fin 2) (x : Homogenization.Vec 2) : (fderiv ℝ (fun (y : Homogenization.Vec 2) => gradCoord T i (t, y)) x) (b t x) * gradCoord T j (t, x) + gradCoord T i (t, x) * (fderiv ℝ (fun (y : Homogenization.Vec 2) => gradCoord T j (t, y)) x) (b t x) = driftTerm b T t i j x

Product rule for the advective terms.

theorem AVenhance.Infra.Section5.LeftToShow.driftTerm_continuous {T : ℝ → Homogenization.Vec 2 → ℝ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) halfSpace) {t : ℝ} (ht : 0 ≤ t) (i j : Fin 2) : Continuous (driftTerm b T t i j)

theorem AVenhance.Infra.Section5.LeftToShow.integral_driftTerm_eq_zero {T : ℝ → Homogenization.Vec 2 → ℝ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) (hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), Flow.spatialDivergence b t x = 0) (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) halfSpace) (hTper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (T t)) {t : ℝ} (ht : 0 ≤ t) (i j : Fin 2) : ∫ (x : Homogenization.Vec 2) in unitCube, driftTerm b T t i j x = 0

The advective terms integrate to zero for a divergence-free periodic drift.

theorem AVenhance.Infra.Section5.LeftToShow.hasDerivAt_integral_gradProduct {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) (hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), Flow.spatialDivergence b t x = 0) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (hTper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (T t)) {t : ℝ} (ht : 0 < t) (i j : Fin 2) : HasDerivAt (fun (s : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, spaceGrad (T s) x i * spaceGrad (T s) x j) (∫ (x : Homogenization.Vec 2) in unitCube, materialGrad b T t x i * spaceGrad (T t) x j + spaceGrad (T t) x i * materialGrad b T t x j) t

∂_t ∫ ∂_iT ∂_jT = ∫ (D_t∂_iT ∂_jT + ∂_iT D_t∂_jT) for a divergence-free periodic drift.