High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Duality.CubeProjectionStabilityDischarge

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

Discharging the cube projection stability

The positive-direction input of the cube Hodge estimate is proved from material:

• existence of the zero-trace identity-coefficient solution of div (∇v − psi) = 0 on the open cube (exists_isZeroTraceDirichletRhsWeakSolution_of_potentialZeroTraceClosureRealization through the convex-domain closure realization);
• the fractional Calderón--Zygmund estimate for that solution on an origin cube (centeredCubeH10ScalarDivergence_fractional_cz_full);
• the two norm bridges cubeEuclideanWspFullENorm_two_sq_eq_hsNormSq and the packaging of a finite-fractional field as a cube Wsp ∩ L² field.

noncomputable def HCPolySupport.HighContrast.RowSupply.wspL2FieldOfHsNormSq {d : ℕ} (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (G : Vec d → Vec d) (hGmeas : MeasureTheory.AEStronglyMeasurable G (MeasureTheory.volume.restrict (openCubeSet Q))) (hGfinite : hsNormSq (openCubeSet Q) s G ≠ ⊤) : CubeEuclideanWspL2Field Q ⟨s, ⋯⟩ FiniteLpExponent.two

Packaging of a measurable field of finite normalized H^s norm as a cube Wsp ∩ L² field. (The construction of the same content is private at its file; it is reproved here rather than imported.)

Equations

• HCPolySupport.HighContrast.RowSupply.wspL2FieldOfHsNormSq Q hs hsHalf G hGmeas hGfinite = { toField := G, euclideanMemLp := ⋯, euclideanMemWsp := ⋯, euclideanMemL2 := ⋯ }

theorem HCPolySupport.HighContrast.RowSupply.exists_cubeGradientProjectionHsStability_originCube (d : ℕ) [NeZero d] : ∃ (Cproj : ℝ), 0 ≤ Cproj ∧ ∀ (m : ℤ) {s : ℝ}, 0 < s → s < 1 / 2 → CubeGradientProjectionHsStability d (originCube d m) s Cproj

The cube projection stability is proved. Every admissible test on an origin cube splits into a zero-trace potential part and a solenoidal remainder, with the potential part H^s-bounded by the test, at a constant fixed before the scale, the order and the test.