CutoffLimitDatum

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

Uniform bounds on the truncated Dirichlet solutions with a datum pass to the full field

The renormalization estimate of the generator is stated for the Dirichlet solutions of the truncated coefficient fields a_L, at every truncation scale L above the cube scale, while the displacement bounds are read at the full stream field a = ν I + k. This file transfers an almost-everywhere bound, valid uniformly in L for the truncated solutions of a Dirichlet problem with a prescribed H¹ datum and a prescribed forcing, to the solution of the same problem for the full field.

The mechanism is the one of the exit-time comparison, with the datum carried along. Two solutions of the same problem for two coefficient fields differ by a zero-trace function, and the energy estimate bounds the gradient of that difference by the supremum distance of the two coefficient fields times the energy of one solution; the zero-trace Poincaré inequality turns this into an L² bound on the values; the distance between a_L (normalized at the origin, a constant skew shift that does not change the equation) and a on a fixed cube is geometric in L; and an almost-everywhere bound holding along an L²-convergent family passes to its limit.

Main results

• sqrt_energy_grad_sub_le_of_h10Diff — the energy estimate for two solutions of the same problem whose difference is a prescribed zero-trace function.
• tendsto_l2_cutoff_of_h10Diff — the truncated solutions converge in L² to the full-field solution, for a common datum and a common forcing.
• ae_abs_sub_le_of_cutoff_bounds — a uniform almost-everywhere bound on the truncated solutions holds for the full-field solution.

References

• ABK26, the passage L → ∞ from the truncated fields a_L to a, and the renormalization of the generator.

1. The energy estimate for two solutions with the same datum

theorem Algsuperdiff.Section5.Provider.sqrt_energy_grad_sub_le_of_h10Diff {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {a b : HCPolySupport.CoeffField d} {lam Lam delta : ℝ} (hdelta : 0 ≤ delta) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam (Support.cubeSetAt y n) a) (hab : ∀ x ∈ Support.cubeSetAt y n, ∀ (i j : Fin d), |a x i j - b x i j| ≤ delta) {u v : HCPolySupport.H1Function (Support.cubeSetAt y n)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hbv : HCPolySupport.MemVectorL2 (Support.cubeSetAt y n) fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (b x) (v.grad x)) (w : HCPolySupport.H10Function (Support.cubeSetAt y n)) (hwg : ∀ (x : HCPolySupport.Vec d), w.grad x = u.grad x - v.grad x) (hu : Section4.Support.IsDivFormWeakSolutionOn a (Support.cubeSetAt y n) u g) (hv : Section4.Support.IsDivFormWeakSolutionOn b (Support.cubeSetAt y n) v g) : √(∫ (x : HCPolySupport.Vec d) in Support.cubeSetAt y n, ‖u.grad x - v.grad x‖ ^ 2) ≤ lam⁻¹ * (↑d * ↑d * delta) * √(∫ (x : HCPolySupport.Vec d) in Support.cubeSetAt y n, ‖v.grad x‖ ^ 2)

The energy estimate for two solutions of the same divergence-form problem for two coefficient fields, when their difference is a prescribed zero-trace function. The gradient of the difference is bounded by the supremum distance of the two coefficient fields, times the energy of the second solution, divided by the lower ellipticity constant of the first field.

2. L² convergence of the truncated solutions

theorem Algsuperdiff.Section5.Provider.tendsto_sqrt_energy_grad_cutoff_of_h10Diff {d : ℕ} (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (y : HCPolySupport.Vec d) (n : ℤ) {h : HCPolySupport.H1Function (Support.cubeSetAt y n)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {u : ℤ → HCPolySupport.H1Function (Support.cubeSetAt y n)} {v : HCPolySupport.H1Function (Support.cubeSetAt y n)} (hu : ∀ (L : ℤ), Section4.Support.HasZeroTraceDifferenceOn (Support.cubeSetAt y n) (u L) h) (huw : ∀ (L : ℤ), Section4.Support.IsDivFormWeakSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L ↑omega).toCoeffField (Support.cubeSetAt y n) (u L) g) (hv : Section4.Support.HasZeroTraceDifferenceOn (Support.cubeSetAt y n) v h) (hvw : Section4.Support.IsDivFormWeakSolutionOn (Field.streamCoefficient M.nu omega) (Support.cubeSetAt y n) v g) : Filter.Tendsto (fun (L : ℤ) => √(∫ (x : HCPolySupport.Vec d) in Support.cubeSetAt y n, ‖(u L).grad x - v.grad x‖ ^ 2)) Filter.atTop (nhds 0)

Gradients of cutoff solutions with common datum and forcing converge in L².

theorem Algsuperdiff.Section5.Provider.tendsto_l2_cutoff_of_h10Diff {d : ℕ} (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (y : HCPolySupport.Vec d) (n : ℤ) {h : HCPolySupport.H1Function (Support.cubeSetAt y n)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {u : ℤ → HCPolySupport.H1Function (Support.cubeSetAt y n)} {v : HCPolySupport.H1Function (Support.cubeSetAt y n)} (hu : ∀ (L : ℤ), Section4.Support.HasZeroTraceDifferenceOn (Support.cubeSetAt y n) (u L) h) (huw : ∀ (L : ℤ), Section4.Support.IsDivFormWeakSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L ↑omega).toCoeffField (Support.cubeSetAt y n) (u L) g) (hv : Section4.Support.HasZeroTraceDifferenceOn (Support.cubeSetAt y n) v h) (hvw : Section4.Support.IsDivFormWeakSolutionOn (Field.streamCoefficient M.nu omega) (Support.cubeSetAt y n) v g) : Filter.Tendsto (fun (L : ℤ) => √(∫ (x : HCPolySupport.Vec d) in Support.cubeSetAt y n, ((u L).toFun x - v.toFun x) ^ 2)) Filter.atTop (nhds 0)

The truncated solutions of a Dirichlet problem with a datum converge in L² to the full-field solution. The datum h and the forcing g are the same at every scale; only the coefficient field moves.

3. Uniform bounds on the truncated solutions pass to the full field

theorem Algsuperdiff.Section5.Provider.ae_abs_sub_le_of_cutoff_bounds {d : ℕ} (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (y : HCPolySupport.Vec d) (n : ℤ) (h : HCPolySupport.H1Function (Support.cubeSetAt y n)) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.MemVectorL2 (Support.cubeSetAt y n) g) {f : HCPolySupport.Vec d → ℝ} (hf : HCPolySupport.MemL2On (Support.cubeSetAt y n) f) {K : ℝ} {m₀ : ℤ} (hbound : ∀ (L : ℤ), m₀ ≤ L → ∀ (uL : HCPolySupport.H1Function (Support.cubeSetAt y n)), Section4.Support.HasZeroTraceDifferenceOn (Support.cubeSetAt y n) uL h → Section4.Support.IsDivFormWeakSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L ↑omega).toCoeffField (Support.cubeSetAt y n) uL g → ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (Support.cubeSetAt y n), |uL.toFun x - f x| ≤ K) {v : HCPolySupport.H1Function (Support.cubeSetAt y n)} (hv : Section4.Support.HasZeroTraceDifferenceOn (Support.cubeSetAt y n) v h) (hvw : Section4.Support.IsDivFormWeakSolutionOn (Field.streamCoefficient M.nu omega) (Support.cubeSetAt y n) v g) : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (Support.cubeSetAt y n), |v.toFun x - f x| ≤ K

A uniform almost-everywhere bound on the truncated solutions holds for the full-field solution. If every solution of the Dirichlet problem with datum h and forcing g for the truncated field a_L, at every truncation scale L ≥ m₀, is almost everywhere within K of a square-integrable function f on the cube, then so is every solution of the same problem for the full stream field.