The differentiated classical θ equation in divergence form and its instantaneous torus energy identity.

def AVenhance.Infra.Section4.ThetaDifferentiatedEnergy.thetaEnergyPositiveDomain : Set (ℝ × Homogenization.Vec 2)

Joint time-space domain with strictly positive time.

Equations

• AVenhance.Infra.Section4.ThetaDifferentiatedEnergy.thetaEnergyPositiveDomain = Set.Ioi 0 ×ˢ Set.univ

theorem AVenhance.Infra.Section4.ThetaDifferentiatedEnergy.thetaEnergy_smooth_slice {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → Homogenization.Vec 2 → E} (hf : ContDiffOn ℝ (↑⊤) (Function.uncurry f) thetaEnergyPositiveDomain) {t : ℝ} (ht : 0 < t) : ContDiff ℝ (↑⊤) (f t)

theorem AVenhance.Infra.Section4.theta_classical_solution_eq_zero_of_zero_data {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hκ : 0 < κ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) (hθ₀ : θ₀ = 0) (t : ℝ) : 0 ≤ t → ∀ (x : Homogenization.Vec 2), θ t x = 0

Zero initial data select the zero classical solution by the energy uniqueness theorem.

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

theorem AVenhance.Infra.Section4.theta_stream_flux_pairing_integration_by_parts {g h u : Homogenization.Vec 2 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hh : ContDiff ℝ (↑⊤) h) (hu : ContDiff ℝ (↑⊤) u) (hgp : IsZ2Periodic g) (hhp : IsZ2Periodic h) (hup : IsZ2Periodic u) : (∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad u x) fun (j : Fin 2) => g x * streamVel (fun (x : ℝ) => h) 0 x j) = -∫ (x : Homogenization.Vec 2) in unitCube, u x * Homogenization.vecDot (spaceGrad g x) (streamVel (fun (x : ℝ) => h) 0 x)

The first stream derivative in a commutator term is transferred onto the stream potential by torus integration by parts. This is the skew-symmetric step that makes the q = 1 energy term use only the stream-regularity order-two bound.

theorem AVenhance.Infra.Section4.theta_streamVel_component_sq_le_gradient {h : Homogenization.Vec 2 → ℝ} (x : Homogenization.Vec 2) (j : Fin 2) : streamVel (fun (x : ℝ) => h) 0 x j ^ 2 ≤ Homogenization.vecNormSq (spaceGrad h x)

Each component of the rotated gradient has square bounded by the full gradient energy.

theorem AVenhance.Infra.Section4.theta_first_order_flux_density_abs_le {u h g : Homogenization.Vec 2 → ℝ} {M : ℝ} (hM : 0 ≤ M) (x : Homogenization.Vec 2) (hu : u x ^ 2 ≤ Homogenization.vecNormSq (spaceGrad h x)) (hg : ∀ (j : Fin 2), |spaceGrad g x j| ≤ M) : |u x * Homogenization.vecDot (spaceGrad g x) (streamVel (fun (x : ℝ) => h) 0 x)| ≤ 2 * M * Homogenization.vecNormSq (spaceGrad h x)

The q = 1 energy term becomes a lower-order gradient square after the skew integration by parts.

theorem AVenhance.Infra.Section4.theta_first_order_flux_pairing_abs_le {u h g : Homogenization.Vec 2 → ℝ} {M : ℝ} (hg : ContDiff ℝ (↑⊤) g) (hh : ContDiff ℝ (↑⊤) h) (hu : ContDiff ℝ (↑⊤) u) (hgp : IsZ2Periodic g) (hhp : IsZ2Periodic h) (hup : IsZ2Periodic u) (hM : 0 ≤ M) (hcomp : ∀ (x : Homogenization.Vec 2), u x ^ 2 ≤ Homogenization.vecNormSq (spaceGrad h x)) (hgrad : ∀ (x : Homogenization.Vec 2) (j : Fin 2), |spaceGrad g x j| ≤ M) : |∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad u x) fun (j : Fin 2) => g x * streamVel (fun (x : ℝ) => h) 0 x j| ≤ 2 * M * ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad h x)

The q = 1 commutator flux pairing is controlled by the lower-order gradient energy after periodic integration by parts. This is the sharper first-order estimate used to check the printed analytic recursion.

theorem AVenhance.Infra.Section4.theta_classical_differentiated_energy_pairing {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) {t : ℝ} (ht : 0 < t) (w : List (Fin 2)) : (∫ (x : Homogenization.Vec 2) in unitCube, classicalWordDerivative w (θ t) x * deriv (fun (s : ℝ) => classicalWordDerivative w (θ s) x) t) + κ * ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (classicalWordDerivative w (θ t)) x) = -∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad (classicalWordDerivative w (θ t)) x) (thetaStreamCommutatorFlux w (φ t) (θ t) x)

For every ordered spatial derivative, the differentiated equation is a forced equation in the divergence form generated by the stream potential. The energy pairing is exact, before estimating the flux by the stream-regularity/diffusivity-recursion data.

theorem AVenhance.Infra.Section4.theta_classical_differentiated_transport_energy_pairing {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) {t : ℝ} (ht : 0 < t) (w : List (Fin 2)) : (∫ (x : Homogenization.Vec 2) in unitCube, classicalWordDerivative w (θ t) x * deriv (fun (s : ℝ) => classicalWordDerivative w (θ s) x) t) + κ * ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (classicalWordDerivative w (θ t)) x) = -∫ (x : Homogenization.Vec 2) in unitCube, classicalWordDerivative w (θ t) x * (classicalWordDerivative w (classicalTransport (streamVel φ t) (θ t)) x - Homogenization.vecDot (streamVel φ t x) (spaceGrad (classicalWordDerivative w (θ t)) x))

Equivalent non-divergence energy pairing. The forcing is the transport commutator itself, which is the form used in the normalized derivative recursion.