Time integrated differentiated energy identities and their input bounds.

def AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaTraceDomain : Set (ℝ × Homogenization.Vec 2)

Joint time-space domain with nonnegative time, including the initial trace.

Equations

• AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaTraceDomain = Set.Ici 0 ×ˢ Set.univ

def AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaTraceClosedCell : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

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

theorem AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaTraceClosedCell_compact : IsCompact thetaTraceClosedCell

theorem AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaTrace_unitCube_subset_closedCell : unitCube ⊆ thetaTraceClosedCell

theorem AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaTrace_joint_extension_continuous {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : ContinuousOn f thetaTraceDomain) : Continuous fun (p : ℝ × Homogenization.Vec 2) => f (max p.1 0, p.2)

theorem AVenhance.Infra.Section4.theta_time_parametric_integral_continuousOn {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : ContinuousOn f ThetaIntegratedEnergy.thetaTraceDomain) : ContinuousOn (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, f (t, x)) (Set.Ici 0)

noncomputable def AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaWordJointSlice (w : List (Fin 2)) (ψ : ℝ → Homogenization.Vec 2 → ℝ) (p : ℝ × Homogenization.Vec 2) : ℝ

Evaluate a spatial derivative word of a curried field on joint time-space.

Equations

• AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaWordJointSlice w ψ p = AVenhance.Infra.Section4.classicalWordDerivative w (ψ p.1) p.2

noncomputable def AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaJointStreamVelocity (w : List (Fin 2)) (θ : ℝ → Homogenization.Vec 2 → ℝ) (p : ℝ × Homogenization.Vec 2) (j : Fin 2) : ℝ

Rotated spatial gradient of a derivative word, giving its stream velocity.

Equations

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

noncomputable def AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaJointStreamFlux (w : List (Fin 2)) (φ θ : ℝ → Homogenization.Vec 2 → ℝ) (p : ℝ × Homogenization.Vec 2) (j : Fin 2) : ℝ

Flux assembled from the ordered-word commutator splits of two scalar fields.

Equations

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

theorem AVenhance.Infra.Section4.ThetaIntegratedEnergy.continuousOn_list_sum {α : Type u_1} [TopologicalSpace α] {L : List (α → ℝ)} {s : Set α} (hL : ∀ f ∈ L, ContinuousOn f s) : ContinuousOn L.sum s

theorem AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaListSumEval {α : Type u_1} (L : List (α → ℝ)) (x : α) : L.sum x = (List.map (fun (f : α → ℝ) => f x) L).sum

theorem AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaJointStreamVelocity_continuousOn {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) thetaTraceDomain) (w : List (Fin 2)) (j : Fin 2) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => thetaJointStreamVelocity w θ p j) thetaTraceDomain

theorem AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaJointStreamFlux_continuousOn {φ θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiffOn ℝ (↑⊤) (Function.uncurry φ) thetaTraceDomain) (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) thetaTraceDomain) (w : List (Fin 2)) (j : Fin 2) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => thetaJointStreamFlux w φ θ p j) thetaTraceDomain

theorem AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaJointStreamVelocity_eq_slice {θ : ℝ → Homogenization.Vec 2 → ℝ} (w : List (Fin 2)) {t : ℝ} (x : Homogenization.Vec 2) (j : Fin 2) : thetaJointStreamVelocity w θ (t, x) j = streamVel (fun (x : ℝ) => classicalWordDerivative w (θ t)) 0 x j

theorem AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaJointStreamFlux_eq_slice {φ θ : ℝ → Homogenization.Vec 2 → ℝ} (w : List (Fin 2)) {t : ℝ} (x : Homogenization.Vec 2) : (fun (j : Fin 2) => thetaJointStreamFlux w φ θ (t, x) j) = thetaStreamCommutatorFlux w (φ t) (θ t) x

theorem AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaJointEnergyFluxPairing_continuousOn {φ θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiffOn ℝ (↑⊤) (Function.uncurry φ) thetaTraceDomain) (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) thetaTraceDomain) (w : List (Fin 2)) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (spaceGrad (classicalWordDerivative w (θ p.1)) p.2) fun (j : Fin 2) => thetaJointStreamFlux w φ θ p j) thetaTraceDomain

theorem AVenhance.Infra.Section4.ThetaIntegratedEnergy.thetaJointEnergyGradientNormSq_continuousOn {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) thetaTraceDomain) (w : List (Fin 2)) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecNormSq (spaceGrad (classicalWordDerivative w (θ p.1)) p.2)) thetaTraceDomain

theorem AVenhance.Infra.Section4.theta_classical_differentiated_energy_integrated {φ : ℝ → 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 ^ 2) + 2 * κ * ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (classicalWordDerivative w (θ t)) x) = (∫ (x : Homogenization.Vec 2) in unitCube, classicalWordDerivative w θ₀ x ^ 2) - 2 * ∫ (t : ℝ) in 0..T, ∫ (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)) ∧ (∫ (x : Homogenization.Vec 2) in unitCube, classicalWordDerivative w (θ T) x ^ 2) + 2 * κ * ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (classicalWordDerivative w (θ t)) x) = (∫ (x : Homogenization.Vec 2) in unitCube, classicalWordDerivative w θ₀ x ^ 2) - 2 * ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad (classicalWordDerivative w (θ t)) x) (thetaStreamCommutatorFlux w (φ t) (θ t) x)

Time-integrated energy balance after differentiating the classical equation by an arbitrary ordered spatial word. The endpoint at zero is obtained from continuity of the closed-half-space representative; differentiation is only used on the open positive-time interval.