High-contrast homogenization: Provider.Regularity.LiouvilleCubeRestriction

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Restricting a Liouville-class solution to a finite centered cube

The frozen Liouville carrier is a whole-space value-gradient pair rather than an H1Function. Its growth limit nevertheless forces finite L² value norm on arbitrarily large balls. Together with the local weighted Sobolev class, this realizes the exact representatives as a finite centered-cube solution.

theorem HCPolySupport.HighContrast.IsWeakSolutionOn.mono {d : ℕ} {b : CoeffField d} {U V : Set (Vec d)} {F : Vec d → Vec d} (hUV : U ⊆ V) (h : IsWeakSolutionOn b V F) : IsWeakSolutionOn b U F

A weak equation restricts to a smaller set. Compact support makes the two set integrals equal to the same whole-space integral.

theorem HCPolySupport.HighContrast.exists_large_radius_normalizedL2Norm_ne_top_of_liouvilleGrowth {d : ℕ} {v : Vec d → ℝ} {theta R : ℝ} (hgrowth : Filter.Tendsto (fun (r : ℝ) => ENNReal.ofReal (r ^ (-(1 + theta))) * normalizedL2Norm (euclideanBall d r) v) Filter.atTop (nhds 0)) : ∃ (r : ℝ), R < r ∧ 0 < r ∧ normalizedL2Norm (euclideanBall d r) v ≠ ⊤

The frozen sublinear limit cannot hide an infinite normalized value norm at every large positive radius: the scalar prefactor is then positive and finite, while the product tends to zero.

theorem HCPolySupport.HighContrast.memLp_volumeRestrict_of_normalizedL2Norm_ne_top {d : ℕ} {V : Set (Vec d)} {v : Vec d → ℝ} (hvmeas : MeasureTheory.AEStronglyMeasurable v MeasureTheory.volume) (hVzero : MeasureTheory.volume V ≠ 0) (hVtop : MeasureTheory.volume V ≠ ⊤) (hnorm : normalizedL2Norm V v ≠ ⊤) : MeasureTheory.MemLp v 2 (MeasureTheory.volume.restrict V)

Finite frozen normalized norm on a positive finite-volume set gives the ordinary local L² membership used by H1Function.

theorem HCPolySupport.HighContrast.exists_pos_euclideanBall_superset_openCubeSet {d : ℕ} [NeZero d] (Q : TriadicCube d) : ∃ (R : ℝ), 0 < R ∧ openCubeSet Q ⊆ euclideanBall d R

Every open triadic cube is contained in some positive-radius centered Euclidean ball.

theorem HCPolySupport.HighContrast.memLp_normalizedCubeMeasure_of_liouvilleGrowth {d : ℕ} [NeZero d] {theta : ℝ} {v : Vec d → ℝ} (hvmeas : MeasureTheory.AEStronglyMeasurable v MeasureTheory.volume) (hgrowth : Filter.Tendsto (fun (r : ℝ) => ENNReal.ofReal (r ^ (-(1 + theta))) * normalizedL2Norm (euclideanBall d r) v) Filter.atTop (nhds 0)) (q : ℕ) : MeasureTheory.MemLp v 2 (normalizedCubeMeasure (originCube d ↑q))

The measurable value representative in the frozen growth condition is in normalized L² on every origin cube.

theorem HCPolySupport.HighContrast.memVectorL2_grad_openCubeSet_of_memH1sLoc {d : ℕ} [NeZero d] {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) {v : Vec d → ℝ} {Dv : Vec d → Vec d} (hv : MemH1sLoc b v Dv) (Q : TriadicCube d) : MemVectorL2 (openCubeSet Q) Dv

The gradient representative of a local Sobolev-class pair is an honest vector-valued L² field on every open centered cube, with the ellipticity pair of a ball containing the cube.

theorem HCPolySupport.HighContrast.exists_cubeSolution_eq_representatives_of_memLiouvilleClass {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) {b : CoeffField d} {theta : ℝ} (hb : IsAELocallyUniformlyElliptic b) {v : Vec d → ℝ} {Dv : Vec d → Vec d} (hv : MemLiouvilleClass b theta v Dv) (hcoeff : (a.coeffOn (originCube d m)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (originCube d m))] b) : ∃ (u : Book.Ch03.CubeSolution (originCube d m) a), u.toH1.toFun = v ∧ u.toH1.grad = Dv

A member of the exact frozen Liouville class restricts to a public finite cube solution, preserving both supplied representatives pointwise.