The flow version of the spectral homogeneous H⁻¹ estimate

def AVenhance.Infra.Ergodic.FlowDerivativeNearIdentity {d : ℕ} (X : PeriodicVolumePreservingDiffeomorphism d) : Prop

Pointwise operator-norm form of the source's near-identity condition. The sum controls both the forward and inverse derivatives.

Equations

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

theorem AVenhance.Infra.Ergodic.HMinusOneErgodicFlow.scalarDerivative_opNorm_le_coordEnergy {d : ℕ} (T : Homogenization.Vec d →L[ℝ] ℝ) : ‖T‖ ≤ ↑d * √(∑ i : Fin d, T (Homogenization.basisVec i) ^ 2)

theorem AVenhance.Infra.Ergodic.HMinusOneErgodicFlow.derivative_norm_le_three_halves {d : ℕ} (X : PeriodicVolumePreservingDiffeomorphism d) (hnear : FlowDerivativeNearIdentity X) (x : Homogenization.Vec d) : ‖fderiv ℝ X.toFun x‖ ≤ 3 / 2

theorem AVenhance.Infra.Ergodic.HMinusOneErgodicFlow.scalarDerivative_comp_energy_bound {d : ℕ} (hd : 0 < d) {φ : Homogenization.Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (X : PeriodicVolumePreservingDiffeomorphism d) (hDX : ∀ (x : Homogenization.Vec d), ‖fderiv ℝ X.toFun x‖ ≤ 3 / 2) (x : Homogenization.Vec d) : ∑ i : Fin d, (fderiv ℝ (fun (y : Homogenization.Vec d) => φ (X.toFun y)) x) (Homogenization.basisVec i) ^ 2 ≤ (3 * ↑d ^ 2) ^ 2 * ∑ j : Fin d, (fderiv ℝ φ (X.toFun x)) (Homogenization.basisVec j) ^ 2

theorem AVenhance.Infra.Ergodic.HMinusOneErgodicFlow.periodic_derivative {d : ℕ} {φ : Homogenization.Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hper : IsZPeriodic φ) (x : Homogenization.Vec d) (k : Fin d → ℤ) : fderiv ℝ φ (x + latticeVector k) = fderiv ℝ φ x

noncomputable def AVenhance.Infra.Ergodic.HMinusOneErgodicFlow.coordinateGradientDensity {d : ℕ} (φ : Homogenization.Vec d → ℝ) : Homogenization.Vec d → ℝ

Sum of squares of the coordinate derivatives of a scalar field.

Equations

• AVenhance.Infra.Ergodic.HMinusOneErgodicFlow.coordinateGradientDensity φ x = ∑ i : Fin d, (fderiv ℝ φ x) (Homogenization.basisVec i) ^ 2

theorem AVenhance.Infra.Ergodic.HMinusOneErgodicFlow.coordinateGradientDensity_periodic {d : ℕ} {φ : Homogenization.Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hper : IsZPeriodic φ) : IsZPeriodic (coordinateGradientDensity φ)

theorem AVenhance.Infra.Ergodic.gradientTestMap_le_of_nearIdentity {d : ℕ} (hd : 0 < d) (X : PeriodicVolumePreservingDiffeomorphism d) (hnear : FlowDerivativeNearIdentity X) : have L := 3 * ↑d ^ 2; ∀ (φ : Homogenization.Vec d → ℝ), ContDiff ℝ (↑⊤) φ → IsZPeriodic φ → gradientL2SquaredAverage φ ≤ 1 → (gradientL2SquaredAverage fun (x : Homogenization.Vec d) => L⁻¹ * φ (X.toFun x)) ≤ 1

The near-identity derivative bounds control the rescaled gradient norm of every smooth periodic test after composition with the flow.