High-contrast homogenization:

Provider.PolynomialHomogenization.FractionalBoundaryWeightedSchurRows

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

Schur rows for the fractional boundary kernel

noncomputable def HCPolySupport.HighContrast.fractionalBoundarySchurKernel {d : ℕ} (U : Set (Vec d)) (s : ℝ) (x y : Vec d) : ENNReal

The boundary-weighted fractional Riesz kernel used in the Schur test.

Equations

• HCPolySupport.HighContrast.fractionalBoundarySchurKernel U s x y = HCPolySupport.HighContrast.euclideanBoundaryWeight U s x * ENNReal.ofReal (HCPolySupport.euclideanDist x y ^ (s - ↑d))

theorem HCPolySupport.HighContrast.measurable_fractionalBoundarySchurKernel {d : ℕ} (U : Set (Vec d)) (s : ℝ) : Measurable (Function.uncurry (fractionalBoundarySchurKernel U s))

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

For 0<s<a and s+a<1, the row and column integrals of the boundary-weighted fractional kernel are bounded by the same auxiliary boundary weight, with structural finite constants.