High-contrast homogenization: Provider.PolynomialHomogenization.ConvexBoundaryWeightMoment

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

Negative moments of Euclidean boundary distance

The weak L¹ tail of inverse boundary distance is integrated to control all negative moments of order below one on a ball-sandwiched convex domain.

theorem HCPolySupport.HighContrast.lintegral_rpow_le_of_weakL1_tail {α : Type u_1} [MeasurableSpace α] (ν : MeasureTheory.Measure α) {f : α → ℝ} {p A : ℝ} (hνtop : ν Set.univ ≠ ⊤) (hp0 : 0 < p) (hp1 : p < 1) (hA : 0 < A) (hf0 : 0 ≤ᵐ[ν] f) (hfmeas : AEMeasurable f ν) (htail : ∀ {t : ℝ}, 0 < t → ν {x : α | t < f x} ≤ ENNReal.ofReal (A * t⁻¹) * ν Set.univ) : ∫⁻ (x : α), ENNReal.ofReal (f x ^ p) ∂ν ≤ ν Set.univ * ENNReal.ofReal (A ^ p / (1 - p))

A nonnegative measurable function with a weak L¹ tail has every moment of order strictly between zero and one.

noncomputable def HCPolySupport.HighContrast.euclideanBoundaryWeight {d : ℕ} (U : Set (Vec d)) (p : ℝ) (x : Vec d) : ENNReal

The negative power of Euclidean boundary distance.

Equations

• HCPolySupport.HighContrast.euclideanBoundaryWeight U p x = ENNReal.ofReal (HCPolySupport.HighContrast.euclideanBoundaryDistance U x ^ (-p))

theorem HCPolySupport.HighContrast.measurable_euclideanBoundaryWeight {d : ℕ} (U : Set (Vec d)) (p : ℝ) : Measurable (euclideanBoundaryWeight U p)

noncomputable def HCPolySupport.HighContrast.euclideanBoundaryWeightMoment {d : ℕ} (U : Set (Vec d)) (p : ℝ) : ENNReal

The normalized negative boundary-distance moment.

Equations

• HCPolySupport.HighContrast.euclideanBoundaryWeightMoment U p = HCPolySupport.HighContrast.eVolumeAverage U (HCPolySupport.HighContrast.euclideanBoundaryWeight U p)

theorem HCPolySupport.HighContrast.lintegral_euclideanBoundaryWeight_le {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {rho Rad p : ℝ} (hsand : HasBallSandwich U rho Rad) (hp0 : 0 < p) (hp1 : p < 1) : ∫⁻ (x : Vec d) in U, euclideanBoundaryWeight U p x ≤ MeasureTheory.volume U * ENNReal.ofReal ((↑d / rho) ^ p / (1 - p))

Every boundary-distance moment below order one has an explicit bound.

theorem HCPolySupport.HighContrast.euclideanBoundaryWeightMoment_le {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {rho Rad p : ℝ} (hsand : HasBallSandwich U rho Rad) (hp0 : 0 < p) (hp1 : p < 1) : euclideanBoundaryWeightMoment U p ≤ ENNReal.ofReal ((↑d / rho) ^ p / (1 - p))

theorem HCPolySupport.HighContrast.euclideanBoundaryWeightMoment_two_mul_le {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {rho Rad s : ℝ} (hsand : HasBallSandwich U rho Rad) (hs : s ∈ Set.Ioo 0 (1 / 2)) : euclideanBoundaryWeightMoment U (2 * s) ≤ ENNReal.ofReal ((↑d / rho) ^ (2 * s) / (1 - 2 * s))

Boundary-distance moment at the fractional Hardy exponent 2s.