HomogenizationObservable

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

The homogenization observable of a triadic cube

The stopped-moment bounds of the displacement estimates take as input an observable that is a weak solution of the homogeneous equation -∇ · a ∇u = 0 on a triadic cube for the stream coefficient, has the trace of a smooth compactly supported function bd, agrees with bd off the cube, is bounded, is continuous on the cube, and is measurable. This file constructs such an observable for every centre, every scale and every datum.

The construction has three steps.

• Existence. The Dirichlet problem with the datum bd and vanishing forcing is solved by the Lax–Milgram theorem of the library: the solution is bd + w with w of zero trace, and the skew part of the stream coefficient plays no role since only the coercivity of the symmetric part ν I enters.
• The bound. The weak maximum principle for the homogeneous equation bounds the solution almost everywhere on the cube by the uniform bound of the datum.
• Continuity. The freezing route gives a representative of the solution that is continuous on the open cube; reading the solution through that representative on the cube and through the datum off the cube produces the observable, and the almost-everywhere bound becomes a pointwise one by continuity.

The existence step and the observable are stated for an arbitrary bounded open convex domain, so that the same construction serves the origin cube and its translates. The observable is also returned together with its almost-everywhere identification with the Sobolev solution it was built from, which the corrector estimates consume.

Main results

• exists_h10_isDivFormWeakSolutionOn_add — the Dirichlet problem with an H¹ datum and a square-integrable forcing is solvable for every elliptic coefficient field.
• exists_streamObservable_of_zeroTraceDifference — the observable built from a weak solution of the homogeneous equation with the trace of a bounded continuous datum.

References

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

1. The Dirichlet problem with an H¹ datum

theorem Algsuperdiff.Section5.Provider.exists_h10_isDivFormWeakSolutionOn_add {d : ℕ} [NeZero d] {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hne : U.Nonempty) {a : HCPolySupport.CoeffField d} {lam Lam : ℝ} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (h : HCPolySupport.H1Function U) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.MemVectorL2 U g) : ∃ (w : HCPolySupport.H10Function U), Section4.Support.IsDivFormWeakSolutionOn a U (h + w.toH1Function) g

Solvability of the Dirichlet problem with an H¹ datum. For an elliptic coefficient field on a bounded open convex domain, an H¹ datum h and a square-integrable forcing field g, the problem -∇ · a ∇u = ∇ · g has a solution of the form h + w with w of zero trace. The zero-trace correction solves the problem with the forcing -(a ∇h) - g, by the Lax–Milgram theorem of the library.

theorem Algsuperdiff.Section5.Provider.isScalarForcedWeakSolution_zero_of_isDivFormWeakSolutionOn {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {u : HCPolySupport.H1Function U} (hsol : Section4.Support.IsDivFormWeakSolutionOn a U u fun (x : HCPolySupport.Vec d) => 0) : DivergenceFormProcess.Form.IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => 0) u

The homogeneous divergence-form equation, read as a scalar-forced weak equation with vanishing forcing.

2. The stream coefficient on a bounded domain

theorem Algsuperdiff.Section5.Provider.continuous_streamCoefficient_sub_smul_one {d : ℕ} {gamma : ℝ} (nu : ℝ) (omega : Field.FullSample d gamma) : Continuous fun (x : HCPolySupport.Vec d) => Field.streamCoefficient nu omega x - nu • 1

The skew part of the stream coefficient is continuous.

theorem Algsuperdiff.Section5.Provider.exists_isEllipticFieldOn_streamCoefficient_of_domain {d : ℕ} {gamma nu : ℝ} (hnu : 0 < nu) (omega : Field.FullSample d gamma) {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) : ∃ (Lam : ℝ), HCPolySupport.IsEllipticFieldOn nu Lam U (Field.streamCoefficient nu omega)

The stream coefficient is elliptic on every bounded open convex domain, with lower constant the molecular diffusivity.

3. The observable

theorem Algsuperdiff.Section5.Provider.exists_streamObservable_of_zeroTraceDifference {d : ℕ} [NeZero d] {M : Section3.ABKModel d} {omega : Field.FullSample d M.gamma} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {bd : HCPolySupport.Vec d → ℝ} (hbd : Continuous bd) {N : ℝ} (hbdN : ∀ (x : HCPolySupport.Vec d), |bd x| ≤ N) (hd : HCPolySupport.H1Function U) (hdbd : ∀ (x : HCPolySupport.Vec d), hd.toFun x = bd x) {h u : HCPolySupport.H1Function U} (hhbd : ∀ x ∈ U, h.toFun x = bd x) (hzt : Section4.Support.HasZeroTraceDifferenceOn U u h) (hsol : Section4.Support.IsDivFormWeakSolutionOn (Field.streamCoefficient M.nu omega) U u fun (x : HCPolySupport.Vec d) => 0) : ∃ (uObs : HCPolySupport.Vec d → ℝ) (Y : HCPolySupport.H1Function U), Measurable uObs ∧ (∀ (z : HCPolySupport.Vec d), |uObs z| ≤ N) ∧ (∀ z ∉ U, uObs z = bd z) ∧ ContinuousOn uObs U ∧ (∀ (z : HCPolySupport.Vec d), Y.toFun z = uObs z) ∧ DivergenceFormProcess.Form.IsScalarForcedWeakSolution (Field.streamWholeSpaceAnalyticData M omega).a U (fun (x : HCPolySupport.Vec d) => 0) Y ∧ (HCPolySupport.MemH10 U fun (z : HCPolySupport.Vec d) => uObs z - bd z) ∧ uObs =ᵐ[MeasureTheory.volume.restrict U] u.toFun

The observable built from a weak solution of the homogeneous equation. Given a weak solution u of -∇ · a ∇u = 0 on a bounded open convex domain for the stream coefficient, whose trace is that of an H¹ function h agreeing on the domain with a bounded continuous function bd that is itself the value of an H¹ function hd, there is a bounded measurable function, continuous on the domain and equal to bd off it, which is almost everywhere the solution on the domain, is the value of an H¹ function solving the homogeneous equation, and has the trace of bd.

The bound is the uniform bound of bd, by the weak maximum principle; the continuity is that of the interior representative supplied by the freezing route.