High-contrast homogenization:

Provider.PolynomialHomogenization.IntegrableBoundaryWeightedCenteredHardy

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

Boundary-weighted Hardy estimate for integrable fields

The endpoint estimate is extended from continuous fields to integrable fields. The only pointwise input in the available proof is convergence of averages on the shrinking convex chain. Lebesgue differentiation supplies that convergence almost everywhere, because the displaced Euclidean chain balls have uniformly bounded eccentricity relative to ambient metric balls.

noncomputable def HCPolySupport.HighContrast.normalizedChainMeasure {d : ℕ} (c x : Vec d) (rho : ℝ) (n : ℕ) : MeasureTheory.Measure (Vec d)

Volume restricted to the nth convex fractional chain ball and rescaled by its inverse volume.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.integrableZeroExtension {d : ℕ} (U : Set (Vec d)) (F : Vec d → Vec d) : Vec d → HilbertVec d

The Hilbert-vector representation of F on U, extended by zero outside U.

Equations

• HCPolySupport.HighContrast.integrableZeroExtension U F y = U.indicator (HCPolySupport.HilbertVec.ofVec ∘ F) y

theorem HCPolySupport.HighContrast.ae_tendsto_convexFractionalChainMean_of_integrable {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {c : Vec d} {rho Rad : ℝ} (hrho : 0 < rho) (hRad : 0 < Rad) (hinner : euclideanBallAt c rho ⊆ U) (houter : U ⊆ euclideanBallAt c Rad) {F : Vec d → Vec d} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict U)) : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict U, Filter.Tendsto (fun (n : ℕ) => HilbertVec.ofVec (convexFractionalChainMean c x rho F n)) Filter.atTop (nhds (HilbertVec.ofVec (F x)))

theorem HCPolySupport.HighContrast.exists_euclideanBoundaryWeightedCenteredEnergy_le_fracSeminormSq_of_integrable {d : ℕ} (hd : 1 ≤ d) {rho Rad s : ℝ} (hrho : 0 < rho) (hRad : 0 < Rad) (hs : s ∈ Set.Ioo 0 (1 / 2)) : ∃ (C : ENNReal), C ≠ ⊤ ∧ ∀ (U : Set (Vec d)), IsOpenBoundedConvexDomain U → HasBallSandwich U rho Rad → ∀ (G : Vec d → Vec d), MeasureTheory.Integrable G (MeasureTheory.volume.restrict U) → euclideanBoundaryWeightedCenteredEnergy U (2 * s) G ≤ C * fracSeminormSq U s G

On every ball-sandwiched convex domain, the centered boundary-weighted fractional energy of an integrable field is controlled by its Gagliardo seminorm with a finite structural constant.