High-contrast homogenization: Provider.PolynomialHomogenization.ConvexHardyPositiveRow

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

Positive fractional energy on convex Whitney rows

The positive fractional row energy consists of the inverse-scale local L² term and the same-cell Gagliardo double integral. The local L² term splits into its centered part and the contribution of the domain average. Cross-row disjointness embeds the diagonal double integrals into the fractional energy on the whole domain.

The final existential estimate chooses its finite coefficient before the domain, the Whitney system, and the function. Thus the coefficient depends only on the displayed dimension, fractional order, and sandwich radii.

noncomputable def HCPolySupport.HighContrast.positiveRowNormalizedDomainMeasure {d : ℕ} (U : Set (Vec d)) : MeasureTheory.Measure (Vec d)

Volume restricted to U and rescaled by the inverse of volume U.

Equations

• HCPolySupport.HighContrast.positiveRowNormalizedDomainMeasure U = (MeasureTheory.volume U)⁻¹ • MeasureTheory.volume.restrict U

theorem HCPolySupport.HighContrast.ofReal_vecNormSq_volumeAverageVec_le_eVolumeAverage {d : ℕ} {U : Set (Vec d)} (hUpos : 0 < MeasureTheory.volume U) (hUtop : MeasureTheory.volume U ≠ ⊤) {F : Vec d → Vec d} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict U)) : ENNReal.ofReal (vecNormSq (volumeAverageVec U F)) ≤ eVolumeAverage U fun (x : Vec d) => ENNReal.ofReal (vecNormSq (F x))

Jensen's inequality for the domain volume average, in the extended-real normalization used by the fractional norms.

noncomputable def HCPolySupport.HighContrast.convexHardyPositiveRowAggregationFactor (d : ℕ) (rho Rad s beta : ℝ) (K : ℕ) (n : ℤ) : ENNReal

A common coefficient for the domain-average and centered fractional parts of the complete positive row energy.

Equations

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

noncomputable def HCPolySupport.HighContrast.convexHardyPositiveRowHsShapeFactor (d : ℕ) (Rad s : ℝ) : ENNReal

The shape factor that absorbs the squared domain average into the volume-scaled L² term of the normalized fractional norm.

Equations

• HCPolySupport.HighContrast.convexHardyPositiveRowHsShapeFactor d Rad s = ENNReal.ofReal ((2 * Rad) ^ d) ^ (2 * s / ↑d) + 1

theorem HCPolySupport.HighContrast.convexHardyPositiveRowHsShapeFactor_ne_top {d : ℕ} (hd : 1 ≤ d) {s : ℝ} (hs : 0 ≤ s) (Rad : ℝ) : convexHardyPositiveRowHsShapeFactor d Rad s ≠ ⊤

The shape factor for the normalized fractional norm is finite.

theorem HCPolySupport.HighContrast.ConvexHardyWhitneySystem.mean_add_fracSeminormSq_le_hsNormSq {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} {rho Rad : ℝ} (hRad : 0 < Rad) (system : ConvexHardyWhitneySystem U rho Rad) (hUpos : 0 < MeasureTheory.volume U) (hUtop : MeasureTheory.volume U ≠ ⊤) {F : Vec d → Vec d} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict U)) {s : ℝ} (hs : 0 < s) : ENNReal.ofReal (vecNormSq (volumeAverageVec U F)) + fracSeminormSq U s F ≤ convexHardyPositiveRowHsShapeFactor d Rad s * hsNormSq U s F

The domain mean and fractional seminorm are jointly controlled by the normalized Hˢ norm with a factor depending only on the outer radius.