Space-time estimates for individual stream-form commutator terms.

def AVenhance.Infra.Section4.ThetaFluxEstimates.thetaFluxClosedCell : Set (ℝ × Homogenization.Vec 2)

Closed time-space unit cell used for the temperature flux estimates.

Equations

• AVenhance.Infra.Section4.ThetaFluxEstimates.thetaFluxClosedCell = Set.Icc 0 1 ×ˢ Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Section4.ThetaFluxEstimates.thetaFluxClosedCell_compact : IsCompact thetaFluxClosedCell

theorem AVenhance.Infra.Section4.ThetaFluxEstimates.thetaFlux_timeCube_subset_closedCell : timeCube ⊆ thetaFluxClosedCell

noncomputable def AVenhance.Infra.Section4.thetaWordExtension (u : ℝ → Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (p : ℝ × Homogenization.Vec 2) : ℝ

Extend a nonnegative-time spatial derivative continuously to all joint space-time points by clamping the time coordinate at zero.

Equations

• AVenhance.Infra.Section4.thetaWordExtension u w p = AVenhance.Infra.Section4.classicalWordDerivative w (u (max p.1 0)) p.2

theorem AVenhance.Infra.Section4.thetaWordExtension_continuous {u : ℝ → Homogenization.Vec 2 → ℝ} {w : List (Fin 2)} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) (Set.Ici 0 ×ˢ Set.univ)) : Continuous (thetaWordExtension u w)

theorem AVenhance.Infra.Section4.thetaWordExtension_eq_slice {u : ℝ → Homogenization.Vec 2 → ℝ} {w : List (Fin 2)} (t : ℝ) (ht : 0 < t) (x : Homogenization.Vec 2) : thetaWordExtension u w (t, x) = classicalWordDerivative w (u t) x

noncomputable def AVenhance.Infra.Section4.thetaWordGradientExtension (u : ℝ → Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (p : ℝ × Homogenization.Vec 2) : Homogenization.Vec 2

Continuous joint representative of a component of the gradient of a word derivative.

Equations

• AVenhance.Infra.Section4.thetaWordGradientExtension u w p j = AVenhance.Infra.Section4.thetaWordExtension u (j :: w) p

theorem AVenhance.Infra.Section4.thetaWordGradientExtension_continuous {u : ℝ → Homogenization.Vec 2 → ℝ} {w : List (Fin 2)} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) (Set.Ici 0 ×ˢ Set.univ)) : Continuous (thetaWordGradientExtension u w)

theorem AVenhance.Infra.Section4.thetaWordGradientExtension_eq_slice {u : ℝ → Homogenization.Vec 2 → ℝ} {w : List (Fin 2)} (t : ℝ) (ht : 0 < t) (x : Homogenization.Vec 2) : thetaWordGradientExtension u w (t, x) = spaceGrad (classicalWordDerivative w (u t)) x

noncomputable def AVenhance.Infra.Section4.thetaStreamWordExtension (u : ℝ → Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (p : ℝ × Homogenization.Vec 2) : Homogenization.Vec 2

The joint stream velocity formed from the gradient of a word derivative.

Equations

• AVenhance.Infra.Section4.thetaStreamWordExtension u w p j = if j = 0 then -AVenhance.Infra.Section4.thetaWordExtension u (1 :: w) p else AVenhance.Infra.Section4.thetaWordExtension u (0 :: w) p

theorem AVenhance.Infra.Section4.thetaStreamWordExtension_continuous {u : ℝ → Homogenization.Vec 2 → ℝ} {w : List (Fin 2)} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) (Set.Ici 0 ×ˢ Set.univ)) : Continuous (thetaStreamWordExtension u w)

theorem AVenhance.Infra.Section4.thetaStreamWordExtension_eq_slice {u : ℝ → Homogenization.Vec 2 → ℝ} {w : List (Fin 2)} (t : ℝ) (ht : 0 < t) (x : Homogenization.Vec 2) : thetaStreamWordExtension u w (t, x) = streamVel (fun (x : ℝ) => classicalWordDerivative w (u t)) 0 x

theorem AVenhance.Infra.Section4.ThetaFluxEstimates.thetaWord_gradient_energy_eq_components {u : ℝ → Homogenization.Vec 2 → ℝ} {w : List (Fin 2)} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) (Set.Ici 0 ×ˢ Set.univ)) : thetaWordSpaceTimeGradientEnergy u w = ∑ j : Fin 2, ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, thetaWordExtension u (j :: w) p ^ 2

theorem AVenhance.Infra.Section4.thetaWordGradientExtension_energy_eq {u : ℝ → Homogenization.Vec 2 → ℝ} {w : List (Fin 2)} : thetaWordSpaceTimeGradientEnergy u w = ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, Homogenization.vecNormSq (thetaWordGradientExtension u w p)

theorem AVenhance.Infra.Section4.theta_word_derivative_energy_le_gradient {u : ℝ → Homogenization.Vec 2 → ℝ} {right word : List (Fin 2)} {i : Fin 2} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) (Set.Ici 0 ×ˢ Set.univ)) (hperm : word.Perm (i :: right)) : ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, thetaWordExtension u word p ^ 2 ≤ thetaWordSpaceTimeGradientEnergy u right

A coordinate derivative obtained by inserting one direction into a word is bounded in space-time L² by the full gradient energy of that word.