HomogenizationCorrector

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

The corrector estimates of the displacement bounds at the stream field

The renormalization of the generator compares, at every truncation scale L above the cube scale m, the Dirichlet solutions of the truncated coefficient field a_L on the origin cube □_m with the solutions of the homogenized problem, almost everywhere on the cube. The two readings of that estimate at the linear datum e ⬝ x and at the quadratic datum (e ⬝ x)² are stated in StoppedMomentsDatum.lean; this file carries them from the truncated fields to the full stream field a = ν I + k, on the triadic cube centred at the origin.

Two ingredients are combined. The renormalization families are assembled from the frozen renormalization theorem with the corrector clause retained, so that the error random variable whose moments are controlled is the same one the corrector clause is stated for. And a bound holding for every truncated solution uniformly in L passes to the full-field solution by the L² convergence of the truncated solutions.

Main results

• exists_renormalizationFamily_corrector — the renormalization families over the scales, with the corrector clause of the frozen theorem retained for the same error family.
• affineH1, quadraticH1 — the two data as H¹ functions of a triadic cube.
• isDirichletSolutionOn_castH1_of_cubeSetAt_zero — the Dirichlet problem on the cube centred at the origin, read on the origin cube.
• ae_abs_sub_affineObservable_le_stream, ae_abs_sub_quadraticObservable_le_stream — the two corrector estimates at the stream field, almost everywhere on the cube.

References

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

1. The renormalization families with the corrector clause retained

theorem Algsuperdiff.Section5.Provider.exists_renormalizationFamily_corrector (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∃ (sigmaBar : ℤ → ℝ) (EB : ℤ → Section3.Cutoff.CutoffSample d → ℝ), (∀ (m : ℤ), 0 < sigmaBar m) ∧ (∀ (m : ℤ), |sigmaBar m - Support.effectiveDiffusivity M.nu cstar M.gamma (3 ^ m)| ≤ C * √M.gamma * |Real.log M.gamma| * sigmaBar m) ∧ (∀ (m : ℤ) (omega : Section3.Cutoff.CutoffSample d), 0 ≤ EB m omega) ∧ (∀ (m : ℤ), Measurable (EB m)) ∧ (∀ (m : ℤ) (p : ℝ), 1 ≤ p → p ≤ C⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (EB m omega) ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ p) ∧ ∀ (m : ℤ), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (L : ℤ), m ≤ L → ∀ (u v h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg Kh KhInf : ℝ), Section4.Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u h g → Section4.Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigmaBar m • 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 m omega * ((sigmaBar m)⁻¹ * Real.rpow 3 (↑m / 2) * Kg + (KhInf + Real.rpow 3 (↑m / 2) * Kh))

The renormalization families over the scales, with the corrector clause. For each scale the frozen renormalization theorem supplies an effective diffusivity and an error random variable; choice over the integers assembles them into two families. The corrector clause of the theorem is retained for that same error family, so that the estimate the displacement bounds consume and the moments of the error are statements about one and the same random variable.

2. The two data as H¹ functions of a triadic cube

theorem Algsuperdiff.Section5.Provider.contDiff_affineObservable {d : ℕ} (n : WithTop ℕ∞) (e : HCPolySupport.Vec d) : ContDiff ℝ n (affineObservable e)

The linear observable is smooth.

theorem Algsuperdiff.Section5.Provider.contDiff_quadraticObservable {d : ℕ} (n : WithTop ℕ∞) (e : HCPolySupport.Vec d) : ContDiff ℝ n (quadraticObservable e)

The quadratic observable is smooth.

theorem Algsuperdiff.Section5.Provider.continuous_affineObservable {d : ℕ} (e : HCPolySupport.Vec d) : Continuous (affineObservable e)

The linear observable is continuous.

theorem Algsuperdiff.Section5.Provider.continuous_quadraticObservable {d : ℕ} (e : HCPolySupport.Vec d) : Continuous (quadraticObservable e)

The quadratic observable is continuous.

noncomputable def Algsuperdiff.Section5.Provider.affineH1 {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (e : HCPolySupport.Vec d) : HCPolySupport.H1Function (Support.cubeSetAt y n)

The linear datum e ⬝ x as an H¹ function of the cube y + □_n.

Equations

• Algsuperdiff.Section5.Provider.affineH1 y n e = HCPolySupport.H1Function.ofContDiffOnIsOpenBoundedConvexDomain ⋯ ⋯

noncomputable def Algsuperdiff.Section5.Provider.quadraticH1 {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (e : HCPolySupport.Vec d) : HCPolySupport.H1Function (Support.cubeSetAt y n)

The quadratic datum (e ⬝ x)² as an H¹ function of the cube y + □_n.

Equations

• Algsuperdiff.Section5.Provider.quadraticH1 y n e = HCPolySupport.H1Function.ofContDiffOnIsOpenBoundedConvexDomain ⋯ ⋯

theorem Algsuperdiff.Section5.Provider.affineH1_grad {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (e : HCPolySupport.Vec d) : (affineH1 y n e).grad = affineGradient e

theorem Algsuperdiff.Section5.Provider.quadraticH1_grad {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (e : HCPolySupport.Vec d) : (quadraticH1 y n e).grad = quadraticGradient e

3. The cube centred at the origin, read on the origin cube

theorem Algsuperdiff.Section5.Provider.isDirichletSolutionOn_castH1_of_cubeSetAt_zero {d : ℕ} {m : ℤ} {a : HCPolySupport.CoeffField d} {u h : HCPolySupport.H1Function (Support.cubeSetAt 0 m)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hzt : Section4.Support.HasZeroTraceDifferenceOn (Support.cubeSetAt 0 m) u h) (hw : Section4.Support.IsDivFormWeakSolutionOn a (Support.cubeSetAt 0 m) u g) : Section4.Support.IsDirichletSolutionOn a (HCPolySupport.originCube d m) (Support.castH1 ⋯ u) (Support.castH1 ⋯ h) g

The Dirichlet problem on the cube centred at the origin is the Dirichlet problem on the origin cube. The two sets are equal, and the H¹ functions are transported along that equality with their values and gradients unchanged.

4. The corrector estimates at the stream field

theorem Algsuperdiff.Section5.Provider.ae_abs_sub_affineObservable_le_stream {d : ℕ} (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (m : ℤ) {sigmaBarM EBm : ℝ} (hren : ∀ (L : ℤ), m ≤ L → ∀ (u v h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg Kh KhInf : ℝ), Section4.Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L ↑omega).toCoeffField (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| ≤ EBm * (sigmaBarM⁻¹ * Real.rpow 3 (↑m / 2) * Kg + (KhInf + Real.rpow 3 (↑m / 2) * Kh))) (e : HCPolySupport.Vec d) {u : HCPolySupport.H1Function (Support.cubeSetAt 0 m)} (hzt : Section4.Support.HasZeroTraceDifferenceOn (Support.cubeSetAt 0 m) u (affineH1 0 m e)) (hw : Section4.Support.IsDivFormWeakSolutionOn (Field.streamCoefficient M.nu omega) (Support.cubeSetAt 0 m) u fun (x : HCPolySupport.Vec d) => 0) : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (Support.cubeSetAt 0 m), |u.toFun x - affineObservable e x| ≤ 3 ^ m * (EBm * ‖e‖)

The corrector estimate at the linear datum, for the stream field. On the triadic cube centred at the origin, a weak solution of the homogeneous equation for the stream coefficient with the trace of the linear datum e ⬝ x is almost everywhere within 3^m EB ‖e‖ of that datum, provided the corrector clause of the renormalization theorem holds at the sample for the scale m with the error value EB and the effective diffusivity sigmaBarM.

theorem Algsuperdiff.Section5.Provider.ae_abs_sub_quadraticObservable_le_stream {d : ℕ} (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (m : ℤ) {sigmaBarM EBm : ℝ} (hsigma : 0 < sigmaBarM) (hren : ∀ (L : ℤ), m ≤ L → ∀ (u v h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg Kh KhInf : ℝ), Section4.Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L ↑omega).toCoeffField (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| ≤ EBm * (sigmaBarM⁻¹ * Real.rpow 3 (↑m / 2) * Kg + (KhInf + Real.rpow 3 (↑m / 2) * Kh))) (e : HCPolySupport.Vec d) {u : HCPolySupport.H1Function (Support.cubeSetAt 0 m)} (hzt : Section4.Support.HasZeroTraceDifferenceOn (Support.cubeSetAt 0 m) u (quadraticH1 0 m e)) (hw : Section4.Support.IsDivFormWeakSolutionOn (Field.streamCoefficient M.nu omega) (Support.cubeSetAt 0 m) u (quadraticForcing sigmaBarM e)) : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (Support.cubeSetAt 0 m), |u.toFun x - quadraticObservable e x| ≤ (3 ^ m) ^ 2 * (5 * EBm * (‖e‖ * vecCoordSum e))

The corrector estimate at the quadratic datum, for the stream field. On the triadic cube centred at the origin, a weak solution of -∇ · a ∇u = ∇ · g for the stream coefficient, with the forcing g = -2 sigmaBarM (e ⬝ x) e and the trace of the quadratic datum (e ⬝ x)², is almost everywhere within 5 (3^m)² EB ‖e‖ (∑ |e_i|) of that datum, under the corrector clause of the renormalization theorem at the sample for the scale m.