High-contrast homogenization: Provider.PolynomialHomogenization.FractionalBoundaryWeightedSchur

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

Schur bound for the fractional boundary kernel

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

A globally positive version of the auxiliary boundary weight. It agrees with the boundary weight on the restricted measure used by the Schur test.

Equations

• HCPolySupport.HighContrast.fractionalBoundarySchurWeight U a x = if x ∈ U then HCPolySupport.HighContrast.euclideanBoundaryWeight U a x else 1

theorem HCPolySupport.HighContrast.measurable_fractionalBoundarySchurWeight {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (a : ℝ) : Measurable (fractionalBoundarySchurWeight U a)

theorem HCPolySupport.HighContrast.exists_lintegral_fractionalBoundarySchurKernel_rpow_two_le {d : ℕ} (hd : 1 ≤ d) {rho Rad s a : ℝ} (hrho : 0 < rho) (hRad : 0 < Rad) (hs : 0 < s) (hsa : s < a) (hsa1 : s + a < 1) : ∃ (C : ENNReal), C ≠ ⊤ ∧ ∀ (U : Set (Vec d)), IsOpenBoundedConvexDomain U → HasBallSandwich U rho Rad → ∀ (f : Vec d → ENNReal), Measurable f → ∫⁻ (x : Vec d) in U, (∫⁻ (y : Vec d) in U, fractionalBoundarySchurKernel U s x y * f y) ^ 2 ≤ C * ∫⁻ (y : Vec d) in U, f y ^ 2

The boundary-weighted fractional Riesz operator satisfies a squared L² Schur bound for every auxiliary exponent s<a<1-s.