Forced torus energy calculations for the actual classical increments.

def AVenhance.Infra.Section4.IteratesEnergy.iterateClosedCell : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

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

theorem AVenhance.Infra.Section4.IteratesEnergy.iterateClosedCell_compact : IsCompact iterateClosedCell

theorem AVenhance.Infra.Section4.IteratesEnergy.iterateUnitCube_subset_closedCell : unitCube ⊆ iterateClosedCell

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

theorem AVenhance.Infra.Section4.IteratesEnergy.iterate_measurableSet_unitCube : MeasurableSet unitCube

theorem AVenhance.Infra.Section4.IteratesEnergy.iterateUnitCell_subset_closedCell : Torus.unitCell 2 ⊆ iterateClosedCell

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

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

theorem AVenhance.Infra.Section4.IteratesEnergy.iterate_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.IteratesEnergy.iterate_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.IteratesEnergy.iterate_spaceGrad_periodic {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hper : IsZ2Periodic f) : IsZ2Periodic (spaceGrad f)

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

theorem AVenhance.Infra.Section4.IteratesEnergy.iterate_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.IteratesEnergy.iterate_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.IteratesEnergy.iterate_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.iterate_classical_energy_pairing {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ F : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hsol : IsClassicalSol (streamVel φ) κ F θ₀ θ) {t : ℝ} (ht : 0 < t) (hF : Continuous (F t)) : (∫ (x : Homogenization.Vec 2) in unitCube, θ t x * deriv (fun (s : ℝ) => θ s x) t) + κ * ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (θ t) x) = ∫ (x : Homogenization.Vec 2) in unitCube, θ t x * F t x

Instantaneous energy identity with the actual forcing retained.

theorem AVenhance.Infra.Section4.iterate_divergence_pairing {u : Homogenization.Vec 2 → ℝ} {H : Homogenization.Vec 2 → Homogenization.Vec 2} (hu : ContDiff ℝ (↑⊤) u) (hup : IsZ2Periodic u) (hH : ContDiff ℝ (↑⊤) H) (hHp : IsZ2Periodic H) : ∫ (x : Homogenization.Vec 2) in unitCube, u x * vecDiv H x = -∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad u x) (H x)

Torus integration by parts for a smooth periodic vector forcing.

theorem AVenhance.Infra.Section4.IteratesEnergy.iterate_young_scalar {κ a b : ℝ} (hκ : 0 < κ) : -(a * b) ≤ κ / 2 * a ^ 2 + (2 * κ)⁻¹ * b ^ 2

theorem AVenhance.Infra.Section4.iterate_young_vector {κ : ℝ} (hκ : 0 < κ) (a b : Homogenization.Vec 2) : -Homogenization.vecDot a b ≤ κ / 2 * Homogenization.vecNormSq a + (2 * κ)⁻¹ * Homogenization.vecNormSq b

Pointwise forcing control with the dissipation coefficient retained.

theorem AVenhance.Infra.Section4.iterate_matrix_flux_bound {A : Matrix (Fin 2) (Fin 2) ℝ} {D : ℝ} (hA : ∀ (i j : Fin 2), |A i j| ≤ D) (v : Homogenization.Vec 2) : Homogenization.vecNormSq (A.mulVec v) ≤ 4 * D ^ 2 * Homogenization.vecNormSq v

Entrywise coefficient control bounds the actual vector flux in dimension two.

theorem AVenhance.Infra.Section4.iterate_matrix_pairing_abs_bound {ρ D : ℝ} (hρ : 0 < ρ) (A : Matrix (Fin 2) (Fin 2) ℝ) (a b : Homogenization.Vec 2) (hA : ∀ (i j : Fin 2), |A i j| ≤ D) : |Homogenization.vecDot a (A.mulVec b)| ≤ ρ * Homogenization.vecNormSq a + D ^ 2 / ρ * Homogenization.vecNormSq b

A matrix forcing pairing can absorb any positive amount of dissipation.

theorem AVenhance.Infra.Section4.IteratesEnergy.iterate_pair_continuous {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {a b : Homogenization.Vec 2 → Homogenization.Vec 2} (hA : Continuous A) (ha : Continuous a) (hb : Continuous b) : Continuous fun (x : Homogenization.Vec 2) => Homogenization.vecDot (a x) ((A x).mulVec (b x))

theorem AVenhance.Infra.Section4.iterate_constant_matrix_pairing_ibp {u v : Homogenization.Vec 2 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hv : ContDiff ℝ (↑⊤) v) (hup : IsZ2Periodic u) (hvp : IsZ2Periodic v) (Q : Matrix (Fin 2) (Fin 2) ℝ) : ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad u x) (Q.mulVec (spaceGrad v x)) = -∫ (x : Homogenization.Vec 2) in unitCube, u x * ∑ i : Fin 2, ∑ j : Fin 2, Q i j * spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad v y j) x i

Transfer the current increment's gradient onto the preceding increment in the constant-matrix boundary pairing of the primitive argument.

theorem AVenhance.Infra.Section4.iterate_matrix_contraction_sq_bound (Q H : Matrix (Fin 2) (Fin 2) ℝ) {D : ℝ} (hQ : ∀ (i j : Fin 2), |Q i j| ≤ D) : (∑ i : Fin 2, ∑ j : Fin 2, Q i j * H i j) ^ 2 ≤ 4 * D ^ 2 * ∑ i : Fin 2, ∑ j : Fin 2, H i j ^ 2

The second-derivative contraction costs only the four matrix entries.

theorem AVenhance.Infra.Section4.IteratesEnergy.iterate_young_abs_scalar {ρ a b : ℝ} (hρ : 0 < ρ) : |a * b| ≤ ρ * a ^ 2 + (4 * ρ)⁻¹ * b ^ 2

theorem AVenhance.Infra.Section4.iterate_primitive_boundary_pairing_bound {u v : Homogenization.Vec 2 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hv : ContDiff ℝ (↑⊤) v) (hup : IsZ2Periodic u) (hvp : IsZ2Periodic v) (Q : Matrix (Fin 2) (Fin 2) ℝ) {ρ D : ℝ} (hρ : 0 < ρ) (hQ : ∀ (i j : Fin 2), |Q i j| ≤ D) : |∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad u x) (Q.mulVec (spaceGrad v x))| ≤ (ρ * ∫ (x : Homogenization.Vec 2) in unitCube, u x ^ 2) + D ^ 2 / ρ * ∫ (x : Homogenization.Vec 2) in unitCube, ∑ i : Fin 2, ∑ j : Fin 2, spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad v y j) x i ^ 2

The boundary term from time integration by parts is controlled by current L² energy and preceding second derivatives, without a pointwise current-gradient norm.

theorem AVenhance.Infra.Section4.iterate_laplacian_pairing_transfer {u v : Homogenization.Vec 2 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hv : ContDiff ℝ (↑⊤) v) (hup : IsZ2Periodic u) (hvp : IsZ2Periodic v) : ∫ (x : Homogenization.Vec 2) in unitCube, spaceLap u x * v x = ∫ (x : Homogenization.Vec 2) in unitCube, u x * spaceLap v x

Periodic self-adjointness transfers the two Laplacian derivatives onto the preceding scalar derivative in the current material equation.

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

theorem AVenhance.Infra.Section4.iterate_vector_laplacian_pairing_transfer {a b : Homogenization.Vec 2 → Homogenization.Vec 2} (ha : ContDiff ℝ (↑⊤) a) (hb : ContDiff ℝ (↑⊤) b) (hap : IsZ2Periodic a) (hbp : IsZ2Periodic b) (Q : Matrix (Fin 2) (Fin 2) ℝ) : ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (fun (i : Fin 2) => spaceLap (fun (y : Homogenization.Vec 2) => a y i) x) (Q.mulVec (b x)) = ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (a x) (Q.mulVec fun (j : Fin 2) => spaceLap (fun (y : Homogenization.Vec 2) => b y j) x)

Constant-matrix Laplacian transfer for vector fields, including the actual gradient fields in the current material equation.