Ordered spatial derivatives at adjacent orders.

This is the pointwise component estimate used for the first-derivative commutator group in the differentiated energy calculation: an order-n+1 coordinate derivative is a component of the gradient of an order-n coordinate derivative.

def AVenhance.Infra.Section4.ThetaEnergy.thetaClosedCell : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Section4.ThetaEnergy.thetaClosedCell = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Section4.ThetaEnergy.thetaClosedCell_compact : IsCompact thetaClosedCell

theorem AVenhance.Infra.Section4.ThetaEnergy.thetaUnitCube_subset_closedCell : unitCube ⊆ thetaClosedCell

theorem AVenhance.Infra.Section4.ThetaEnergy.theta_integrableOn_unitCube {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f unitCube MeasureTheory.volume

theorem AVenhance.Infra.Section4.ThetaEnergy.theta_measurableSet_unitCube : MeasurableSet unitCube

theorem AVenhance.Infra.Section4.ThetaEnergy.thetaUnitCell_subset_closedCell : Torus.unitCell 2 ⊆ thetaClosedCell

theorem AVenhance.Infra.Section4.ThetaEnergy.theta_integrableOn_unitCell {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f (Torus.unitCell 2) MeasureTheory.volume

theorem AVenhance.Infra.Section4.ThetaEnergy.theta_realToComplex_periodic {f : Homogenization.Vec 2 → ℝ} (hper : IsZ2Periodic f) : Torus.IsZdPeriodic (Torus.realToComplex f)

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

theorem AVenhance.Infra.Section4.ThetaEnergy.theta_integral_unitCube_coord_ibp {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hpf : IsZ2Periodic f) (hpg : IsZ2Periodic g) (i : Fin 2) : ∫ (x : Homogenization.Vec 2) in unitCube, f x * spaceGrad g x i = -∫ (x : Homogenization.Vec 2) in unitCube, spaceGrad f x i * g x

theorem AVenhance.Infra.Section4.ThetaEnergy.theta_spaceGrad_periodic {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hper : IsZ2Periodic f) : IsZ2Periodic (spaceGrad f)

theorem AVenhance.Infra.Section4.ThetaEnergy.theta_spaceGrad_contDiff {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (spaceGrad f)

theorem AVenhance.Infra.Section4.ThetaEnergy.theta_mixed_partial_commute {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad f y 0) x 1 = spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad f y 1) x 0

theorem AVenhance.Infra.Section4.ThetaEnergy.theta_spaceGrad_mul {f g : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (i : Fin 2) (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) : spaceGrad (fun (y : Homogenization.Vec 2) => f y * g y) x i = spaceGrad f x i * g x + f x * spaceGrad g x i

theorem AVenhance.Infra.Section4.ThetaEnergy.theta_streamVel_components {φ : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} {x : Homogenization.Vec 2} : streamVel φ t x 0 = -spaceGrad (φ t) x 1 ∧ streamVel φ t x 1 = spaceGrad (φ t) x 0

theorem AVenhance.Infra.Section4.theta_laplacian_pairing {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : IsZ2Periodic f) : ∫ (x : Homogenization.Vec 2) in unitCube, f x * spaceLap f x = -∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad f x)

The spatial Laplacian contributes exactly the negative Dirichlet energy when paired with a smooth periodic function on the unit torus cell.

theorem AVenhance.Infra.Section4.theta_stream_drift_pairing_zero {φ u : Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφper : IsZ2Periodic φ) (hu : ContDiff ℝ (↑⊤) u) (huper : IsZ2Periodic u) : ∫ (x : Homogenization.Vec 2) in unitCube, u x * Homogenization.vecDot (streamVel (fun (x : ℝ) => φ) 0 x) (spaceGrad u x) = 0

A stream drift makes no contribution to the scalar energy pairing. The proof expands the two coordinates, integrates each cross term by parts, and uses symmetry of the stream Hessian.

theorem AVenhance.Infra.Section4.theta_divergence_pairing {u : Homogenization.Vec 2 → ℝ} {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hu : ContDiff ℝ (↑⊤) u) (huper : IsZ2Periodic u) (hF : ContDiff ℝ (↑⊤) F) (hFper : IsZ2Periodic F) : ∫ (x : Homogenization.Vec 2) in unitCube, u x * vecDiv F x = -∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad u x) (F x)

Periodic integration by parts for the divergence of a smooth vector field.

theorem AVenhance.Infra.Section4.theta_forced_classical_energy_pairing {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {F : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hφ : IsAdmissibleStream φ) {t : ℝ} (hu : ContDiff ℝ (↑⊤) (u t)) (huper : IsZ2Periodic (u t)) (hF : ContDiff ℝ (↑⊤) (F t)) (hFper : IsZ2Periodic (F t)) (hpde : ∀ (x : Homogenization.Vec 2), deriv (fun (s : ℝ) => u s x) t - κ * spaceLap (u t) x + Homogenization.vecDot (streamVel φ t x) (spaceGrad (u t) x) = vecDiv (F t) x) : (∫ (x : Homogenization.Vec 2) in unitCube, u t x * deriv (fun (s : ℝ) => u s x) t) + κ * ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (u t) x) = -∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad (u t) x) (F t x)

A smooth periodic forced equation in divergence form has the usual instantaneous energy pairing. The forcing enters through its flux, as in the commutator equation for differentiated θ.

theorem AVenhance.Infra.Section4.ordered_derivative_eq_gradient_component {n : ℕ} {f : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (i : Fin (n + 1) → Fin 2) (h : DifferentiableAt ℝ (iteratedFDeriv ℝ n f) x) : ((iteratedFDeriv ℝ (n + 1) f x) fun (j : Fin (n + 1)) => Homogenization.basisVec (i j)) = spaceGrad (fun (y : Homogenization.Vec 2) => (iteratedFDeriv ℝ n f y) fun (j : Fin n) => Homogenization.basisVec (i j.succ)) x (i 0)

The ordered derivative with first direction i 0 is the corresponding component of the gradient of the derivative in the remaining directions.