The corrected L² ergodic estimate

def AVenhance.Infra.Ergodic.AveragesL2.coordinateLine {d : ℕ} (i : Fin d) (x : Homogenization.Vec d) (t : ℝ) : Homogenization.Vec d

Coordinate line through a point, parametrized in the chosen basis direction.

Equations

• AVenhance.Infra.Ergodic.AveragesL2.coordinateLine i x t = x + t • Homogenization.basisVec i

theorem AVenhance.Infra.Ergodic.AveragesL2.coordinateLine_hasDerivAt {d : ℕ} (i : Fin d) (x : Homogenization.Vec d) (t : ℝ) : HasDerivAt (coordinateLine i x) (Homogenization.basisVec i) t

theorem AVenhance.Infra.Ergodic.AveragesL2.coordinateLine_contDiff {d : ℕ} (i : Fin d) (x : Homogenization.Vec d) : ContDiff ℝ (↑⊤) (coordinateLine i x)

theorem AVenhance.Infra.Ergodic.AveragesL2.coordDerivIter_line_hasDerivAt {d : ℕ} (i : Fin d) (n : ℕ) {f : Homogenization.Vec d → ℂ} (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec d) (t : ℝ) : HasDerivAt (fun (s : ℝ) => coordDerivIter i n f (coordinateLine i x s)) (Torus.coordDeriv i (coordDerivIter i n f) (coordinateLine i x t)) t

theorem AVenhance.Infra.Ergodic.iteratedDeriv_coordinateLine {d : ℕ} (i : Fin d) (n : ℕ) {f : Homogenization.Vec d → ℂ} (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec d) (t : ℝ) : iteratedDeriv n (fun (s : ℝ) => f (AveragesL2.coordinateLine i x s)) t = coordDerivIter i n f (AveragesL2.coordinateLine i x t)

theorem AVenhance.Infra.Ergodic.coordDerivIter_mul {d : ℕ} (i : Fin d) (n : ℕ) {f g : Homogenization.Vec d → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (x : Homogenization.Vec d) : coordDerivIter i n (fun (y : Homogenization.Vec d) => f y * g y) x = ∑ j ∈ Finset.range (n + 1), ↑(n.choose j) * coordDerivIter i j f x * coordDerivIter i (n - j) g x

def AVenhance.Infra.Ergodic.HasCoordinateAnalyticL2Bounds {d : ℕ} (f : Homogenization.Vec d → ℂ) (Cf r : ℝ) : Prop

Factorial analytic bounds for all coordinate derivatives in the unit-cell L² norm.

Equations

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

def AVenhance.Infra.Ergodic.AveragesL2.closedUnitCube (d : ℕ) : Set (Homogenization.Vec d)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Ergodic.AveragesL2.closedUnitCube d = Set.univ.pi fun (x : Fin d) => Set.Icc 0 1

theorem AVenhance.Infra.Ergodic.AveragesL2.unitCell_subset_closedUnitCube (d : ℕ) : Torus.unitCell d ⊆ closedUnitCube d

theorem AVenhance.Infra.Ergodic.AveragesL2.isCompact_closedUnitCube (d : ℕ) : IsCompact (closedUnitCube d)

theorem AVenhance.Infra.Ergodic.continuous_unitCell_integrable {d : ℕ} {u : Homogenization.Vec d → ℝ} (hu : Continuous u) : MeasureTheory.IntegrableOn u (Torus.unitCell d) MeasureTheory.volume

theorem AVenhance.Infra.Ergodic.continuous_unitCell_memLp_two {d : ℕ} {u : Homogenization.Vec d → ℝ} (hu : Continuous u) : MeasureTheory.MemLp u (ENNReal.ofReal 2) (MeasureTheory.volume.restrict (Torus.unitCell d))

theorem AVenhance.Infra.Ergodic.AveragesL2.factorial_plus_one_le_two_pow (n : ℕ) : n + 1 ≤ 2 ^ n

theorem AVenhance.Infra.Ergodic.AveragesL2.coordDerivIter_square_hasL1Bounds {d : ℕ} {f : Homogenization.Vec d → ℂ} (hf : ContDiff ℝ (↑⊤) f) (Cf r : ℝ) (hCf : 0 ≤ Cf) (hr : 0 < r) (hL2 : HasCoordinateAnalyticL2Bounds f Cf r) : HasCoordinateAnalyticL1Bounds (fun (x : Homogenization.Vec d) => f x * f x) (Cf ^ 2) (r / 2)

theorem AVenhance.Infra.Ergodic.cellAverage_square_mul_sub_le_of_coordinateAnalyticL2Bounds {d N : ℕ} (hd : 0 < d) (hN : 0 < N) {f : Homogenization.Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : IsZPeriodic f) (Cf r : ℝ) (hCf : 0 ≤ Cf) (hr : 0 < r) (hderiv : HasCoordinateAnalyticL2Bounds (fun (x : Homogenization.Vec d) => ↑(f x)) Cf r) {g : Homogenization.Vec d → ℝ} (hg2 : MeasureTheory.LocallyIntegrable (fun (x : Homogenization.Vec d) => |g x| ^ 2) MeasureTheory.volume) (hfast : IsFastPeriodic N g) (hNr : 2 ≤ r * ↑N) : |(cellAverage fun (x : Homogenization.Vec d) => f x ^ 2 * g x ^ 2) - (cellAverage fun (x : Homogenization.Vec d) => f x ^ 2) * cellAverage fun (x : Homogenization.Vec d) => g x ^ 2| ≤ ((512 * Cf ^ 2 * cellAverage fun (x : Homogenization.Vec d) => |g x| ^ 2) * ∑' (k : Fin d → ℤ), Real.exp (-(1 / 1024) * ‖k‖)) * Real.exp (-(r / 2 * ↑N) / 1024)

The square version of the ergodic covariance estimate. The derivative assumption includes order zero, and rN ≥ 2 is needed because the L¹ estimate is applied at radius r / 2.