GeneratorRenormalizationLimit

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

Renormalization of the generator for the coefficient field a = nu I + k

The renormalization estimate of the generator is proved for the infrared truncations a_L = nu I + k_L of the coefficient field, uniformly in the truncation scale L above the cube scale m. This file removes the truncation: the same effective diffusivity sigmaBar_m and the same random error amplitude control the Dirichlet solutions of the full coefficient field a = nu I + k itself, on the carrier of the full sample and under its law.

Two mechanisms are combined. The probabilistic half is a transfer along the inclusion of the full-sample carrier into the carrier of the truncations: the moments of the error amplitude, its measurability, and the almost-sure clause all move along that inclusion with no loss of constant. The analytic half is the limit L -> infinity. For a datum h and a forcing g fixed once and for all, the Dirichlet problem for a_L has a solution u_L with the same datum at every scale, and the energy estimate for the difference of two solutions bounds the gradient of u_L - u by the supremum distance of a_L and a on the cube, which is geometric in L. Hence u_L -> u in H^1, and both clauses of the estimate are closed under that convergence: the uniform clause because an almost-everywhere bound valid along an L^2-convergent family passes to its limit, and the energy clause because the Dirichlet energy is continuous along gradients converging in L^2.

No uniqueness of the Dirichlet solution is used: the solutions u_L are chosen arbitrarily among those with the prescribed datum, and their difference with the given solution u of the full-field problem is a function of zero trace, which is all the energy estimate needs.

Main results

• abs_integral_vecNormSq_sub_le — the Dirichlet energy is continuous in the gradient, with the Cauchy--Schwarz modulus.
• tendsto_sqrt_energy_grad_cutoff_of_h10Diff — the gradients of the truncated solutions converge in L^2 to the gradient of the full-field solution.
• clauses_stream_of_cutoff — the two clauses of the renormalization estimate pass from the truncated fields to the full field.
• generator_renormalization_provider — the renormalization estimate for the coefficient field itself.

References

• ABK26, Theorem B, and the passage L -> infinity from the truncated fields a_L to a = nu I + k.

1. Continuity of the Dirichlet energy in the gradient

theorem Algsuperdiff.Section4.Provider.Introduction.abs_integral_vecNormSq_sub_le {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) {F G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : HCPolySupport.MemVectorL2 U F) (hG : HCPolySupport.MemVectorL2 U G) : |(∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecNormSq (F x)) - ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecNormSq (G x)| ≤ ↑d * (√(∫ (x : HCPolySupport.Vec d) in U, ‖F x - G x‖ ^ 2) * √(∫ (x : HCPolySupport.Vec d) in U, ‖F x - G x‖ ^ 2)) + 2 * (↑d * (√(∫ (x : HCPolySupport.Vec d) in U, ‖F x - G x‖ ^ 2) * √(∫ (x : HCPolySupport.Vec d) in U, ‖G x‖ ^ 2)))

The Dirichlet energy is continuous in the gradient. Two square-integrable fields have energies differing by at most the Cauchy--Schwarz modulus of their difference: expanding |F|² = |F - G|² + 2 (F - G) · G + |G|² and integrating leaves the square of the L² distance plus twice the pairing of that distance with the second field.

2. Convergence of the truncated solutions in the energy norm

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

The gradients of the truncated solutions converge in L² to the gradient of the full-field solution, for a common datum and a common forcing. The difference of the two solutions is a function of zero trace, so the energy estimate bounds its gradient by the supremum distance of the two coefficient fields on the cube, which is geometric in the truncation scale.

3. The two clauses pass to the full field

theorem Algsuperdiff.Section4.Provider.Introduction.clauses_stream_of_cutoff {d : ℕ} (M : Section3.ABKModel d) (omega : Section5.Field.FullSample d M.gamma) (m : ℤ) (V : Set (HCPolySupport.Vec d)) (hV : Section5.Support.cubeSetAt 0 m = V) {sigmaBarM Binf BE : ℝ} {u v h : HCPolySupport.H1Function V} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.MemVectorL2 V g) (hren : ∀ (L : ℤ), m ≤ L → ∀ (uL : HCPolySupport.H1Function V), Support.HasZeroTraceDifferenceOn V uL h → Support.IsDivFormWeakSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L ↑omega).toCoeffField V uL g → (∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict V, Real.rpow 3 (-↑m) * |uL.toFun x - v.toFun x| ≤ Binf) ∧ |(HCPolySupport.volumeAverage V fun (y : HCPolySupport.Vec d) => M.nu * HCPolySupport.vecNormSq (uL.grad y)) - HCPolySupport.volumeAverage V fun (y : HCPolySupport.Vec d) => sigmaBarM * HCPolySupport.vecNormSq (v.grad y)| ≤ BE) (hzt : Support.HasZeroTraceDifferenceOn V u h) (hw : Support.IsDivFormWeakSolutionOn (Section5.Field.streamCoefficient M.nu omega) V u g) : (∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict V, Real.rpow 3 (-↑m) * |u.toFun x - v.toFun x| ≤ Binf) ∧ |(HCPolySupport.volumeAverage V fun (y : HCPolySupport.Vec d) => M.nu * HCPolySupport.vecNormSq (u.grad y)) - HCPolySupport.volumeAverage V fun (y : HCPolySupport.Vec d) => sigmaBarM * HCPolySupport.vecNormSq (v.grad y)| ≤ BE

The two clauses of the renormalization estimate pass from the truncated coefficient fields to the full stream field. The datum h, the homogenized solution v and the forcing g are fixed; the hypothesis is that both clauses hold, with the same two right-hand sides, for every solution of the truncated problem with that datum and that forcing at every truncation scale above m. The uniform clause passes to the limit because an almost-everywhere bound along an L²-convergent family is inherited by the limit; the energy clause passes because the Dirichlet energy is continuous along gradients converging in L². The cube is presented as an arbitrary set equal to the cube centred at the origin, so that the estimate can be read on the origin cube of the renormalization statement.

4. The transfers along the inclusion of the full-sample carrier

5. The renormalization estimate for the coefficient field

theorem Algsuperdiff.Section4.Provider.Introduction.generator_renormalization_provider (d : ℕ) (cstar : ℝ) (_hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (m : ℤ), ∃ (sigmaBarM : ℝ), 0 < sigmaBarM ∧ |sigmaBarM - √(M.nu ^ 2 + cstar * M.gamma⁻¹ * Real.rpow 3 (2 * M.gamma * ↑m))| ≤ C * √M.gamma * |Real.log M.gamma| * sigmaBarM ∧ ∃ (EB : Section5.Field.FullSample d M.gamma → ℝ), (∀ (omega : Section5.Field.FullSample d M.gamma), 0 ≤ EB omega) ∧ Measurable EB ∧ (∀ (p : ℝ), 1 ≤ p → p ≤ C⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (omega : Section5.Field.FullSample d M.gamma), ENNReal.ofReal (EB omega) ^ p ∂↑(Section5.Field.fullSampleLaw M) ≤ ENNReal.ofReal (C * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ p) ∧ ∀ᵐ (omega : Section5.Field.FullSample d M.gamma) ∂↑(Section5.Field.fullSampleLaw M), ∀ (u v h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg Kh KhInf : ℝ), Support.IsDirichletSolutionOn (Section5.Field.streamCoefficient M.nu omega) (HCPolySupport.originCube d m) u h g → Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigmaBarM • 1) (HCPolySupport.originCube d m) v h g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad x‖ ≤ KhInf) → 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 omega * (sigmaBarM⁻¹ * Real.rpow 3 (↑m / 2) * Kg + (KhInf + Real.rpow 3 (↑m / 2) * Kh))) ∧ |(HCPolySupport.volumeAverage (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (y : HCPolySupport.Vec d) => M.nu * HCPolySupport.vecNormSq (u.grad y)) - HCPolySupport.volumeAverage (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (y : HCPolySupport.Vec d) => sigmaBarM * HCPolySupport.vecNormSq (v.grad y)| ≤ EB omega * (√sigmaBarM⁻¹ * Real.rpow 3 (↑m / 2) * Kg + √sigmaBarM * (KhInf + Real.rpow 3 (↑m / 2) * Kh)) ^ 2

Renormalization of the generator for the coefficient field a = nu I + k. At every scale m there are an effective diffusivity sigmaBar_m, close to sqrt (nu ^ 2 + cstar gamma⁻¹ 3 ^ (2 gamma m)) in the relative sense, and a random error amplitude with Gaussian-type moments, such that on the cube □_m the solution of the Dirichlet problem for the coefficient field and the solution of the homogenized problem with the same datum and the same forcing are close, both uniformly and in Dirichlet energy.