Higher spatial derivatives of the classical theta equation.

def AVenhance.Infra.Section4.ThetaDifferentiated.thetaTimeDir : ℝ × Homogenization.Vec 2

Pure time direction used to differentiate the temperature equation.

Equations

• AVenhance.Infra.Section4.ThetaDifferentiated.thetaTimeDir = (1, 0)

def AVenhance.Infra.Section4.ThetaDifferentiated.thetaSpaceDir (i : Fin 2) : ℝ × Homogenization.Vec 2

Pure spatial coordinate direction used to differentiate the temperature equation.

Equations

• AVenhance.Infra.Section4.ThetaDifferentiated.thetaSpaceDir i = (0, Homogenization.basisVec i)

def AVenhance.Infra.Section4.ThetaDifferentiated.thetaJointPositiveDomain : Set (ℝ × Homogenization.Vec 2)

Joint time-space domain with strictly positive time.

Equations

• AVenhance.Infra.Section4.ThetaDifferentiated.thetaJointPositiveDomain = Set.Ioi 0 ×ˢ Set.univ

def AVenhance.Infra.Section4.thetaJointWordDerivative : List (Fin 2) → (ℝ × Homogenization.Vec 2 → ℝ) → ℝ × Homogenization.Vec 2 → ℝ

Ordered spatial derivatives of a scalar function on the joint time-space domain.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section4.thetaJointWordDerivative [] x✝ = x✝

noncomputable def AVenhance.Infra.Section4.thetaJointTimePartial (f : ℝ × Homogenization.Vec 2 → ℝ) : ℝ × Homogenization.Vec 2 → ℝ

Time partial derivative of a scalar function on joint time-space.

Equations

• AVenhance.Infra.Section4.thetaJointTimePartial f p = (fderiv ℝ f p) AVenhance.Infra.Section4.ThetaDifferentiated.thetaTimeDir

theorem AVenhance.Infra.Section4.thetaJointTimePartial_contDiffOn {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : ContDiffOn ℝ (↑⊤) f ThetaDifferentiated.thetaJointPositiveDomain) : ContDiffOn ℝ (↑⊤) (thetaJointTimePartial f) ThetaDifferentiated.thetaJointPositiveDomain

theorem AVenhance.Infra.Section4.thetaJointWordDerivative_contDiffOn {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : ContDiffOn ℝ (↑⊤) f ThetaDifferentiated.thetaJointPositiveDomain) (w : List (Fin 2)) : ContDiffOn ℝ (↑⊤) (thetaJointWordDerivative w f) ThetaDifferentiated.thetaJointPositiveDomain

theorem AVenhance.Infra.Section4.theta_joint_spatial_section_derivative {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) ThetaDifferentiated.thetaJointPositiveDomain) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) (i : Fin 2) : spaceGrad (u t) x i = (fderiv ℝ (Function.uncurry u) (t, x)) (0, Homogenization.basisVec i)

Differentiating a spatial slice is evaluation of the joint derivative in the corresponding spatial direction.

theorem AVenhance.Infra.Section4.theta_time_spatial_partial_commute {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) ThetaDifferentiated.thetaJointPositiveDomain) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) (i : Fin 2) : ((fderiv ℝ (fderiv ℝ (Function.uncurry u)) (t, x)) (0, Homogenization.basisVec i)) (1, 0) = ((fderiv ℝ (fderiv ℝ (Function.uncurry u)) (t, x)) (1, 0)) (0, Homogenization.basisVec i)

The time and spatial coordinate derivatives of a jointly smooth function commute.

theorem AVenhance.Infra.Section4.thetaJointWordDerivative_eq_classicalWordDerivative {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) ThetaDifferentiated.thetaJointPositiveDomain) (w : List (Fin 2)) {t : ℝ} : 0 < t → ∀ (x : Homogenization.Vec 2), thetaJointWordDerivative w (Function.uncurry u) (t, x) = classicalWordDerivative w (u t) x

The ordered joint derivatives restrict to the paper's ordered spatial coordinate derivatives on every positive-time slice.

theorem AVenhance.Infra.Section4.thetaJointWordDerivative_timePartial {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : ContDiffOn ℝ (↑⊤) f ThetaDifferentiated.thetaJointPositiveDomain) (w : List (Fin 2)) (p : ℝ × Homogenization.Vec 2) : p ∈ ThetaDifferentiated.thetaJointPositiveDomain → thetaJointWordDerivative w (thetaJointTimePartial f) p = thetaJointTimePartial (thetaJointWordDerivative w f) p

Any ordered collection of spatial derivatives commutes with the time partial of a jointly smooth function on positive time.

theorem AVenhance.Infra.Section4.classicalWordDerivative_timePartial_commute {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) ThetaDifferentiated.thetaJointPositiveDomain) {t : ℝ} (ht : 0 < t) (w : List (Fin 2)) (x : Homogenization.Vec 2) : classicalWordDerivative w (fun (y : Homogenization.Vec 2) => classicalTimePartial u (t, y)) x = classicalTimePartial (fun (s : ℝ) (y : Homogenization.Vec 2) => classicalWordDerivative w (u s) y) (t, x)

The ordinary time derivative commutes with any ordered spatial word for a classical function that is jointly smooth at positive time.

theorem AVenhance.Infra.Section4.classicalWordDerivative_add (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : (classicalWordDerivative w fun (x : Homogenization.Vec 2) => f x + g x) = fun (x : Homogenization.Vec 2) => classicalWordDerivative w f x + classicalWordDerivative w g x

theorem AVenhance.Infra.Section4.classicalWordDerivative_sub (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : (classicalWordDerivative w fun (x : Homogenization.Vec 2) => f x - g x) = fun (x : Homogenization.Vec 2) => classicalWordDerivative w f x - classicalWordDerivative w g x

theorem AVenhance.Infra.Section4.ThetaDifferentiated.classicalSpaceGrad_const_mul (c : ℝ) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => c * f y) x i = c * spaceGrad f x i

theorem AVenhance.Infra.Section4.ThetaDifferentiated.thetaSpaceGradComponent_contDiff {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i : Fin 2) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => spaceGrad f x i

theorem AVenhance.Infra.Section4.classicalWordDerivative_const_mul (w : List (Fin 2)) (c : ℝ) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) : (classicalWordDerivative w fun (x : Homogenization.Vec 2) => c * f x) = fun (x : Homogenization.Vec 2) => c * classicalWordDerivative w f x

theorem AVenhance.Infra.Section4.classicalWordDerivative_spaceLap (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) : classicalWordDerivative w (spaceLap f) = spaceLap (classicalWordDerivative w f)

theorem AVenhance.Infra.Section4.ThetaDifferentiated.theta_smooth_joint_slice {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ × Homogenization.Vec 2 → E} (hf : ContDiffOn ℝ (↑⊤) f thetaJointPositiveDomain) {t : ℝ} (ht : 0 < t) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => f (t, x)

theorem AVenhance.Infra.Section4.ThetaDifferentiated.theta_spaceLap_contDiff {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (spaceLap f)

theorem AVenhance.Infra.Section4.ThetaDifferentiated.theta_transport_contDiff {b : Homogenization.Vec 2 → Homogenization.Vec 2} {u : Homogenization.Vec 2 → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ (↑⊤) (classicalTransport b u)

theorem AVenhance.Infra.Section4.ThetaDifferentiated.classicalWordDerivative_zero (w : List (Fin 2)) : (classicalWordDerivative w fun (x : Homogenization.Vec 2) => 0) = fun (x : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Section4.theta_classical_differentiated_transport_equation {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) (hb : ContDiffOn ℝ (↑⊤) (Function.uncurry b) ThetaDifferentiated.thetaJointPositiveDomain) {t : ℝ} (ht : 0 < t) (w : List (Fin 2)) (x : Homogenization.Vec 2) : classicalTimePartial (fun (s : ℝ) (y : Homogenization.Vec 2) => classicalWordDerivative w (θ s) y) (t, x) - κ * spaceLap (classicalWordDerivative w (θ t)) x + classicalTransport (b t) (classicalWordDerivative w (θ t)) x + ∑ j : Fin 2, classicalWordCommutatorExpansion w (fun (y : Homogenization.Vec 2) => b t y j) (fun (y : Homogenization.Vec 2) => spaceGrad (θ t) y j) x = 0

The classical equation differentiated along an arbitrary ordered spatial word. The last term is exactly the finite transport commutator expansion.

theorem AVenhance.Infra.Section4.ThetaDifferentiated.list_sum_fin_sum_swap {α : Type u_1} (L : List α) (F : Fin 2 → α → ℝ) : ∑ j : Fin 2, (List.map (fun (a : α) => F j a) L).sum = (List.map (fun (a : α) => ∑ j : Fin 2, F j a) L).sum

theorem AVenhance.Infra.Section4.ThetaDifferentiated.list_sum_zero_of_forall {α : Type u_1} (L : List α) (f : α → ℝ) (hf : ∀ a ∈ L, f a = 0) : (List.map f L).sum = 0

theorem AVenhance.Infra.Section4.ThetaDifferentiated.thetaDifferentiated_streamVel_components {φ : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} : streamVel (fun (x : ℝ) => φ) 0 x 0 = -spaceGrad φ x 1 ∧ streamVel (fun (x : ℝ) => φ) 0 x 1 = spaceGrad φ x 0

theorem AVenhance.Infra.Section4.theta_streamVel_ordered_derivative_divergence_free (φ : Homogenization.Vec 2 → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) (w : List (Fin 2)) (x : Homogenization.Vec 2) : ∑ j : Fin 2, spaceGrad (classicalWordDerivative w fun (y : Homogenization.Vec 2) => streamVel (fun (x : ℝ) => φ) 0 y j) x j = 0

Every ordered spatial derivative of a two-dimensional stream velocity is divergence free. This is the cancellation that turns the differentiated transport commutator into a divergence flux.

theorem AVenhance.Infra.Section4.classicalWordDerivative_streamVel_component (w : List (Fin 2)) (φ : Homogenization.Vec 2 → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) (j : Fin 2) : (classicalWordDerivative w fun (y : Homogenization.Vec 2) => streamVel (fun (x : ℝ) => φ) 0 y j) = fun (y : Homogenization.Vec 2) => streamVel (fun (x : ℝ) => classicalWordDerivative w φ) 0 y j

Ordered derivatives commute through the stream velocity's single coordinate gradient.

theorem AVenhance.Infra.Section4.theta_streamVel_contDiff (φ : Homogenization.Vec 2 → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) : ContDiff ℝ (↑⊤) (streamVel (fun (x : ℝ) => φ) 0)

Smoothness of the vector field generated by a smooth stream function.

theorem AVenhance.Infra.Section4.ThetaDifferentiated.theta_spaceGrad_component_periodic {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : IsZ2Periodic f) (i : Fin 2) : IsZ2Periodic fun (x : Homogenization.Vec 2) => spaceGrad f x i

theorem AVenhance.Infra.Section4.classicalWordDerivative_periodic (w : List (Fin 2)) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : IsZ2Periodic f) : IsZ2Periodic (classicalWordDerivative w f)

Ordered coordinate derivatives preserve spatial periodicity.

theorem AVenhance.Infra.Section4.theta_streamVel_periodic (φ : Homogenization.Vec 2 → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) (hper : IsZ2Periodic φ) : IsZ2Periodic (streamVel (fun (x : ℝ) => φ) 0)

Spatial periodicity of a stream velocity follows by differentiating the periodicity of its scalar stream function.

theorem AVenhance.Infra.Section4.ThetaDifferentiated.theta_list_map_sum_congr {α : Type u_1} (L : List α) (f g : α → ℝ) (h : ∀ a ∈ L, f a = g a) : (List.map f L).sum = (List.map g L).sum

theorem AVenhance.Infra.Section4.theta_streamVel_joint_contDiffOn {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) : ContDiffOn ℝ (↑⊤) (Function.uncurry (streamVel φ)) classicalPositiveTimeDomain

The stream velocity is jointly smooth on positive time, using the smooth joint stream potential and its spatial Fréchet derivatives.

noncomputable def AVenhance.Infra.Section4.thetaStreamCommutatorProductTerm (p : List (Fin 2) × List (Fin 2)) (φ u : Homogenization.Vec 2 → ℝ) : Homogenization.Vec 2 → Homogenization.Vec 2

A single stream-form Leibniz term in the differentiated divergence operator.

Equations

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

noncomputable def AVenhance.Infra.Section4.thetaStreamCommutatorFlux (w : List (Fin 2)) (φ u : Homogenization.Vec 2 → ℝ) : Homogenization.Vec 2 → Homogenization.Vec 2

The stream-function flux in the ordered-word commutator expansion.

Equations

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

theorem AVenhance.Infra.Section4.theta_product_vector_divergence {g : Homogenization.Vec 2 → ℝ} {v : Homogenization.Vec 2 → Homogenization.Vec 2} (hg : ContDiff ℝ (↑⊤) g) (hv : ContDiff ℝ (↑⊤) v) (hdiv : ∀ (x : Homogenization.Vec 2), vecDiv v x = 0) (x : Homogenization.Vec 2) : vecDiv (fun (y : Homogenization.Vec 2) (j : Fin 2) => g y * v y j) x = Homogenization.vecDot (spaceGrad g x) (v x)

theorem AVenhance.Infra.Section4.ThetaDifferentiated.theta_streamVel_dot_grad_skew (g h : Homogenization.Vec 2 → ℝ) (x : Homogenization.Vec 2) : Homogenization.vecDot (spaceGrad g x) (streamVel (fun (x : ℝ) => h) 0 x) = -Homogenization.vecDot (streamVel (fun (x : ℝ) => g) 0 x) (spaceGrad h x)

theorem AVenhance.Infra.Section4.ThetaDifferentiated.thetaStreamCommutatorProductTerm_contDiff (p : List (Fin 2) × List (Fin 2)) (φ u : Homogenization.Vec 2 → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ (↑⊤) (thetaStreamCommutatorProductTerm p φ u)

theorem AVenhance.Infra.Section4.thetaStreamCommutatorFlux_contDiff_periodic (w : List (Fin 2)) {φ u : Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hu : ContDiff ℝ (↑⊤) u) (hφper : IsZ2Periodic φ) (huper : IsZ2Periodic u) : ContDiff ℝ (↑⊤) (thetaStreamCommutatorFlux w φ u) ∧ IsZ2Periodic (thetaStreamCommutatorFlux w φ u)

The stream commutator flux is smooth and periodic whenever its two scalar inputs are.

theorem AVenhance.Infra.Section4.thetaStreamCommutatorFlux_divergence (w : List (Fin 2)) (φ u : Homogenization.Vec 2 → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) (hu : ContDiff ℝ (↑⊤) u) (x : Homogenization.Vec 2) : vecDiv (thetaStreamCommutatorFlux w φ u) x = -∑ j : Fin 2, classicalWordCommutatorExpansion w (fun (y : Homogenization.Vec 2) => streamVel (fun (x : ℝ) => φ) 0 y j) (fun (y : Homogenization.Vec 2) => spaceGrad u y j) x

Divergence of the differentiated stream flux is the negative transport commutator. This is the source's skew-symmetric divergence form; it avoids one unnecessary derivative on the stream potential.