RepresentativeComparator

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

The Lipschitz representative of a zero-trace solution with bounded gradient

A zero-trace H¹ function on y + □_n whose stored gradient field is bounded by Ksup at every point of the cube has a Lipschitz representative, and that representative is bounded on the whole cube by d · Ksup · 3^n / 2.

The two constants carry a factor d, which is the price of the supremum norm on Vec d = Fin d → ℝ and is sharp: a linear function whose d partial derivatives all equal Ksup has increments d · Ksup · ‖x - z‖. The second constant is d · Ksup times the distance from a point of the cube to the complement of its closure, which is at most half the side length 3^n.

Main results

• exists_lipschitzRepresentative_of_zeroTrace.
• exists_lipschitzRepresentative_comparator.

References

• ABK26, the localized Dirichlet problems of Section 5.1.

1. Geometry: a nearby point outside the closed cube

theorem Algsuperdiff.Section5.Support.cubeSetAt_subset_cubeSetAt_succ {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : cubeSetAt y n ⊆ cubeSetAt y (n + 1)

2. The representative of a zero-trace solution with bounded gradient

theorem Algsuperdiff.Section5.Support.exists_lipschitzRepresentative_of_zeroTrace {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} (hd : 0 < d) {v : HCPolySupport.H1Function (cubeSetAt y n)} {Ksup : ℝ} (hKsup : 0 ≤ Ksup) (hw : ∃ (w : HCPolySupport.H10Function (cubeSetAt y n)), (∀ (x : HCPolySupport.Vec d), v.toFun x = w.toFun x) ∧ ∀ (x : HCPolySupport.Vec d), v.grad x = w.grad x) (hgrad : ∀ x ∈ cubeSetAt y n, ‖v.grad x‖ ≤ Ksup) : ∃ (vRep : HCPolySupport.Vec d → ℝ), v.toFun =ᵐ[MeasureTheory.volume.restrict (cubeSetAt y n)] vRep ∧ LipschitzWith (↑d * Ksup).toNNReal vRep ∧ supNormOn (cubeSetAt y n) vRep ≤ ENNReal.ofReal (↑d * Ksup * 3 ^ n / 2)

A zero-trace H¹ function whose stored gradient field is bounded on y + □_n has a Lipschitz representative, and that representative is bounded on the whole cube.

Both constants carry the factor d of the supremum-norm geometry; the sup bound is d · Ksup times half the side length, the distance from a point of the cube to the complement of its closure.

3. From the Lipschitz bound to the C^{0,1/2} gauge

theorem Algsuperdiff.Section5.Support.hasCubeContinuousRepresentativeAt_of_zeroTrace {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} (hd : 0 < d) {v : HCPolySupport.H1Function (cubeSetAt y n)} {Ksup : ℝ} (hKsup : 0 ≤ Ksup) (hw : ∃ (w : HCPolySupport.H10Function (cubeSetAt y n)), (∀ (x : HCPolySupport.Vec d), v.toFun x = w.toFun x) ∧ ∀ (x : HCPolySupport.Vec d), v.grad x = w.grad x) (hgrad : ∀ x ∈ cubeSetAt y n, ‖v.grad x‖ ≤ Ksup) : HasCubeContinuousRepresentativeAt y n v

A zero-trace solution with bounded gradient has a representative continuous on the cube.

4. The comparator

theorem Algsuperdiff.Section5.Support.exists_lipschitzRepresentative_comparator (d : ℕ) (hdim : 2 ≤ d) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg : ℝ), Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) Kg g → ∃ (v : HCPolySupport.H1Function (cubeSetAt y n)) (vRep : HCPolySupport.Vec d → ℝ) (Ksup : ℝ) (KHol : ℝ), IsDirichletSolutionAt (fun (x : HCPolySupport.Vec d) => ↑(Section3.Annealed.sigmaBar M n) • 1) y n v g ∧ 0 ≤ Ksup ∧ 0 ≤ KHol ∧ (∀ x ∈ cubeSetAt y n, ‖v.grad x‖ ≤ Ksup) ∧ Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) KHol v.grad ∧ Real.rpow 3 (-(1 / 2 * ↑n)) * Ksup + KHol ≤ C * (Real.rpow 3 (1 / 2 * ↑n))⁻¹ * ((↑(Section3.Annealed.sigmaBar M n))⁻¹ * Real.rpow 3 (↑n / 2) * Kg) ∧ v.toFun =ᵐ[MeasureTheory.volume.restrict (cubeSetAt y n)] vRep ∧ LipschitzWith (↑d * Ksup).toNNReal vRep ∧ supNormOn (cubeSetAt y n) vRep ≤ ENNReal.ofReal (↑d * Ksup * 3 ^ n / 2) ∧ HasCubeContinuousRepresentativeAt y n v

The comparator of Section 5.1 has a Lipschitz representative bounded on the whole cube.

At every scale and centre, and for every 1/2-Hölder forcing field, the constant-coefficient Dirichlet problem -σ_n Δ v = ∇·g on y + □_n with zero boundary values has a solution whose stored gradient field is bounded and 1/2-Hölder, with the interior Schauder estimate, and whose values are those of a d · Ksup-Lipschitz function bounded by d · Ksup · 3^n / 2. In particular the comparator satisfies HasCubeContinuousRepresentativeAt unconditionally.