Ordered-coordinate energy levels and their normalization.

def AVenhance.Infra.Section4.thetaCoordinateWord {n : ℕ} (i : Fin n → Fin 2) : List (Fin 2)

The ordered coordinate word represented by a finite tuple.

Equations

• AVenhance.Infra.Section4.thetaCoordinateWord i = List.ofFn i

@[simp]

theorem AVenhance.Infra.Section4.thetaCoordinateWord_length {n : ℕ} (i : Fin n → Fin 2) : (thetaCoordinateWord i).length = n

noncomputable def AVenhance.Infra.Section4.thetaWordSpatialEnergy (θ : ℝ → Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (t : ℝ) : ℝ

The squared spatial L² norm of one ordered derivative at time t.

Equations

• AVenhance.Infra.Section4.thetaWordSpatialEnergy θ w t = ∫ (x : Homogenization.Vec 2) in AVenhance.unitCube, AVenhance.Infra.Section4.classicalWordDerivative w (θ t) x ^ 2

noncomputable def AVenhance.Infra.Section4.thetaWordSpaceTimeGradientEnergy (θ : ℝ → Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) : ℝ

The squared space-time gradient norm of one ordered derivative.

Equations

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

noncomputable def AVenhance.Infra.Section4.thetaWordSpatialEnergySup (θ : ℝ → Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) : ℝ

The largest spatial energy over the closed unit time interval, expressed as the supremum of the actual classical energy values.

Equations

• AVenhance.Infra.Section4.thetaWordSpatialEnergySup θ w = sSup (Set.range fun (t : { t : ℝ // t ∈ Set.Icc 0 1 }) => AVenhance.Infra.Section4.thetaWordSpatialEnergy θ w ↑t)

theorem AVenhance.Infra.Section4.thetaWordSpatialEnergy_le_sup (θ : ℝ → Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) {t : ℝ} (ht : t ∈ Set.Icc 0 1) (hbounded : BddAbove (Set.range fun (s : { s : ℝ // s ∈ Set.Icc 0 1 }) => thetaWordSpatialEnergy θ w ↑s)) : thetaWordSpatialEnergy θ w t ≤ thetaWordSpatialEnergySup θ w

theorem AVenhance.Infra.Section4.thetaWordSpatialEnergySup_le (θ : ℝ → Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) {B : ℝ} (hB : ∀ t ∈ Set.Icc 0 1, thetaWordSpatialEnergy θ w t ≤ B) : thetaWordSpatialEnergySup θ w ≤ B

noncomputable def AVenhance.Infra.Section4.thetaEnergyLevel (θ : ℝ → Homogenization.Vec 2 → ℝ) (κ : ℝ) (n : ℕ) : ℝ

The level n energy is the maximum over ordered coordinate tuples of the uniform-time L² norm plus the diffusivity-weighted space-time gradient norm.

Equations

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

theorem AVenhance.Infra.Section4.thetaEnergyLevel_le_of_coordinate (θ : ℝ → Homogenization.Vec 2 → ℝ) (κ : ℝ) (n : ℕ) (i : Fin n → Fin 2) : √(thetaWordSpatialEnergySup θ (thetaCoordinateWord i)) + √κ * √(thetaWordSpaceTimeGradientEnergy θ (thetaCoordinateWord i)) ≤ thetaEnergyLevel θ κ n