StoppedMomentsDatum

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The linear and quadratic observables of the displacement bounds

The two Dirichlet problems behind Steps 1 and 3 of the superdiffusive displacement bounds are posed on the origin cube openCubeSet (originCube d m) with the boundary data

  ell_e (x) = e ⬝ x ,          quad_e (x) = (e ⬝ x)^2 ,

and, for the second one, the right-hand side -2 sigma, written as the divergence of the field g(x) = -2 sigma (e ⬝ x) e. The homogenized solutions are the data themselves: ell_e is harmonic, and quad_e satisfies -sigma * Laplacian quad_e = -2 sigma (e ⬝ e), which is exactly the divergence of g.

This file records the calculus these two data need in order to be fed to the renormalization of the generator, and reads its conclusion at each of them.

• Gradients: ell_e has the constant gradient e, and quad_e has the gradient 2 (e ⬝ x) e.
• Hölder data: a field of the form x ↦ (c (e ⬝ x)) e has 1/2-Hölder seminorm at most |c| ‖e‖ (sum of |e_i|) 3^{m/2} on a cube of side 3^m, and is bounded there by |c| ‖e‖ (sum of |e_i|) 3^m / 2. The constant gradient e has vanishing seminorm and is bounded by ‖e‖.
• Homogenized solutions: the two data solve the constant-coefficient problems with the stated forcings. For the linear datum this is one integration by parts against a zero-trace test function; for the quadratic datum the two sides of the weak equation agree pointwise.

Reading the renormalization estimate at these data then gives, on the cube of side 3^m,

  |u - ell_e| <= 3^m * EB * ‖e‖ ,
  |u - quad_e| <= (3^m)^2 * 5 * EB * ‖e‖ * (sum of |e_i|) ,

almost everywhere, the two displays e.u.minus.v.mean and e.u.minus.v.second of the source. The effective diffusivity cancels in the second: the field g carries the factor 2 sigma and the estimate divides by sigma.

Main definitions

• affineObservable, affineGradient — e ⬝ x and its gradient.
• quadraticObservable, quadraticGradient — (e ⬝ x)^2 and its gradient.
• quadraticForcing — the field -2 sigma (e ⬝ x) e.
• vecCoordSum — the sum of the absolute values of the coordinates.

Main results

• hasGradientOn_affineObservable, hasGradientOn_quadraticObservable.
• holderSeminormBoundOn_affineGradient, holderSeminormBoundOn_smulAffineField.
• isDirichletSolutionOn_homogenized_affine, isDirichletSolutionOn_homogenized_quadratic.
• ae_abs_sub_affineObservable_le, ae_abs_sub_quadraticObservable_le.

References

• ABK26, Steps 1 and 3 of the superdiffusive displacement bounds of Section 5.4.

1. The observables

def Algsuperdiff.Section5.Provider.affineObservable {d : ℕ} (e : HCPolySupport.Vec d) : HCPolySupport.Vec d → ℝ

The linear observable x ↦ e ⬝ x.

Equations

• Algsuperdiff.Section5.Provider.affineObservable e x = HCPolySupport.vecDot e x

def Algsuperdiff.Section5.Provider.affineGradient {d : ℕ} (e : HCPolySupport.Vec d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The gradient of the linear observable: the constant field e.

Equations

• Algsuperdiff.Section5.Provider.affineGradient e x✝ = e

def Algsuperdiff.Section5.Provider.quadraticObservable {d : ℕ} (e : HCPolySupport.Vec d) : HCPolySupport.Vec d → ℝ

The quadratic observable x ↦ (e ⬝ x)^2.

Equations

• Algsuperdiff.Section5.Provider.quadraticObservable e x = HCPolySupport.vecDot e x * HCPolySupport.vecDot e x

def Algsuperdiff.Section5.Provider.quadraticGradient {d : ℕ} (e : HCPolySupport.Vec d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The gradient of the quadratic observable: x ↦ 2 (e ⬝ x) e.

Equations

• Algsuperdiff.Section5.Provider.quadraticGradient e x = (2 * HCPolySupport.vecDot e x) • e

def Algsuperdiff.Section5.Provider.quadraticForcing {d : ℕ} (sigma : ℝ) (e : HCPolySupport.Vec d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The field whose divergence is the constant right-hand side of the quadratic problem: g(x) = -2 sigma (e ⬝ x) e.

Equations

• Algsuperdiff.Section5.Provider.quadraticForcing sigma e x = (-(2 * sigma) * HCPolySupport.vecDot e x) • e

def Algsuperdiff.Section5.Provider.vecCoordSum {d : ℕ} (e : HCPolySupport.Vec d) : ℝ

The sum of the absolute values of the coordinates of a vector; it is the constant relating the pairing e ⬝ x to the supremum norm of x.

Equations

• Algsuperdiff.Section5.Provider.vecCoordSum e = ∑ i : Fin d, |e i|

theorem Algsuperdiff.Section5.Provider.vecCoordSum_nonneg {d : ℕ} (e : HCPolySupport.Vec d) : 0 ≤ vecCoordSum e

theorem Algsuperdiff.Section5.Provider.abs_vecDot_le_vecCoordSum_mul {d : ℕ} (e x : HCPolySupport.Vec d) : |HCPolySupport.vecDot e x| ≤ vecCoordSum e * ‖x‖

The pairing against a fixed vector is bounded by the coordinate sum times the supremum norm.

2. The gradients

theorem Algsuperdiff.Section5.Provider.hasGradientOn_affineObservable {d : ℕ} (W : Set (HCPolySupport.Vec d)) (e : HCPolySupport.Vec d) : Section4.Support.HasGradientOn W (affineObservable e) (affineGradient e)

The gradient of the linear observable.

theorem Algsuperdiff.Section5.Provider.hasGradientOn_quadraticObservable {d : ℕ} (W : Set (HCPolySupport.Vec d)) (e : HCPolySupport.Vec d) : Section4.Support.HasGradientOn W (quadraticObservable e) (quadraticGradient e)

The gradient of the quadratic observable.

3. The geometry of the origin cube

theorem Algsuperdiff.Section5.Provider.norm_lt_of_mem_openCubeSet_originCube {d : ℕ} {m : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : ‖x‖ < 1 / 2 * 3 ^ m

The supremum norm on the origin cube of scale m is below half the side length.

theorem Algsuperdiff.Section5.Provider.norm_sub_le_of_mem_openCubeSet_originCube {d : ℕ} {m : ℤ} {x z : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : ‖x - z‖ ≤ 3 ^ m

The diameter of the origin cube of scale m in the supremum norm.

4. The Hölder data

theorem Algsuperdiff.Section5.Provider.holderSeminormBoundOn_affineGradient {d : ℕ} (W : Set (HCPolySupport.Vec d)) (e : HCPolySupport.Vec d) : Section4.Support.HolderSeminormBoundOn W (1 / 2) 0 (affineGradient e)

The constant gradient has vanishing Hölder seminorm.

theorem Algsuperdiff.Section5.Provider.holderSeminormBoundOn_zero_field {d : ℕ} (W : Set (HCPolySupport.Vec d)) : Section4.Support.HolderSeminormBoundOn W (1 / 2) 0 fun (x : HCPolySupport.Vec d) => 0

The vanishing field has vanishing Hölder seminorm.

theorem Algsuperdiff.Section5.Provider.holderSeminormBoundOn_smulAffineField {d : ℕ} (m : ℤ) (c : ℝ) (e : HCPolySupport.Vec d) : Section4.Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) (|c| * (‖e‖ * vecCoordSum e) * Real.rpow 3 (↑m / 2)) fun (x : HCPolySupport.Vec d) => (c * HCPolySupport.vecDot e x) • e

The Hölder seminorm of a field proportional to (e ⬝ x) e on the origin cube.

theorem Algsuperdiff.Section5.Provider.norm_smulAffineField_le {d : ℕ} (m : ℤ) (c : ℝ) (e : HCPolySupport.Vec d) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : ‖(c * HCPolySupport.vecDot e x) • e‖ ≤ |c| * (‖e‖ * vecCoordSum e) * (1 / 2 * 3 ^ m)

The uniform bound for a field proportional to (e ⬝ x) e on the origin cube.

5. The homogenized solutions

theorem Algsuperdiff.Section5.Provider.isDirichletSolutionOn_homogenized_affine {d : ℕ} (sigma : ℝ) (m : ℤ) (e : HCPolySupport.Vec d) (v : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (hvgrad : ∀ (x : HCPolySupport.Vec d), v.grad x = affineGradient e x) : Section4.Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigma • 1) (HCPolySupport.originCube d m) v v fun (x : HCPolySupport.Vec d) => 0

The linear observable solves the homogenized problem with vanishing forcing. The constant-coefficient equation for a constant gradient tests to zero against any zero-trace function, by one integration by parts.

theorem Algsuperdiff.Section5.Provider.isDirichletSolutionOn_homogenized_quadratic {d : ℕ} (sigma : ℝ) (m : ℤ) (e : HCPolySupport.Vec d) (v : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (hvgrad : ∀ (x : HCPolySupport.Vec d), v.grad x = quadraticGradient e x) : Section4.Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigma • 1) (HCPolySupport.originCube d m) v v (quadraticForcing sigma e)

The quadratic observable solves the homogenized problem with the stated forcing. Here the two sides of the weak equation agree pointwise: the forcing field is exactly minus the effective diffusivity times the gradient of the observable.

6. Reading the renormalization estimate at the two data

theorem Algsuperdiff.Section5.Provider.ae_abs_sub_affineObservable_le {d : ℕ} {a : HCPolySupport.CoeffField d} {m : ℤ} {sigmaBarM EB : ℝ} (hren : ∀ (u v h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg Kh KhInf : ℝ), Section4.Support.IsDirichletSolutionOn a (HCPolySupport.originCube d m) u h g → Section4.Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigmaBarM • 1) (HCPolySupport.originCube d m) v h g → Section4.Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → Section4.Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad x‖ ≤ KhInf) → Section4.Support.HasGradientOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) h.toFun h.grad → ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)), Real.rpow 3 (-↑m) * |u.toFun x - v.toFun x| ≤ EB * (sigmaBarM⁻¹ * Real.rpow 3 (↑m / 2) * Kg + (KhInf + Real.rpow 3 (↑m / 2) * Kh))) {e : HCPolySupport.Vec d} {u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))} (hhval : ∀ (x : HCPolySupport.Vec d), h.toFun x = affineObservable e x) (hhgrad : ∀ (x : HCPolySupport.Vec d), h.grad x = affineGradient e x) (hu : Section4.Support.IsDirichletSolutionOn a (HCPolySupport.originCube d m) u h fun (x : HCPolySupport.Vec d) => 0) : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)), |u.toFun x - affineObservable e x| ≤ 3 ^ m * (EB * ‖e‖)

The renormalization estimate at the linear datum. With vanishing forcing, vanishing Hölder seminorm of the constant gradient, and the uniform gradient bound ‖e‖, the estimate reads |u - ell_e| <= 3^m EB ‖e‖.

theorem Algsuperdiff.Section5.Provider.ae_abs_sub_quadraticObservable_le {d : ℕ} {a : HCPolySupport.CoeffField d} {m : ℤ} {sigmaBarM EB : ℝ} (hsigma : 0 < sigmaBarM) (hren : ∀ (u v h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg Kh KhInf : ℝ), Section4.Support.IsDirichletSolutionOn a (HCPolySupport.originCube d m) u h g → Section4.Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigmaBarM • 1) (HCPolySupport.originCube d m) v h g → Section4.Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → Section4.Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad x‖ ≤ KhInf) → Section4.Support.HasGradientOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) h.toFun h.grad → ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)), Real.rpow 3 (-↑m) * |u.toFun x - v.toFun x| ≤ EB * (sigmaBarM⁻¹ * Real.rpow 3 (↑m / 2) * Kg + (KhInf + Real.rpow 3 (↑m / 2) * Kh))) {e : HCPolySupport.Vec d} {u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))} (hhval : ∀ (x : HCPolySupport.Vec d), h.toFun x = quadraticObservable e x) (hhgrad : ∀ (x : HCPolySupport.Vec d), h.grad x = quadraticGradient e x) (hu : Section4.Support.IsDirichletSolutionOn a (HCPolySupport.originCube d m) u h (quadraticForcing sigmaBarM e)) : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)), |u.toFun x - quadraticObservable e x| ≤ (3 ^ m) ^ 2 * (5 * EB * (‖e‖ * vecCoordSum e))

The renormalization estimate at the quadratic datum. The effective diffusivity cancels: the forcing field carries the factor 2 sigma and the estimate divides by sigma. The estimate reads |u - quad_e| <= 5 (3^m)^2 EB ‖e‖ (sum of |e_i|).