High-contrast homogenization: Provider.PolynomialHomogenization.FractionalPotentialSchurAssembly

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

Assembly of a pointwise fractional potential estimate with Schur

noncomputable def HCPolySupport.HighContrast.euclideanBoundaryWeightedEnergyAround {d : ℕ} (U : Set (Vec d)) (p : ℝ) (F : Vec d → Vec d) (m : Vec d) : ENNReal

Boundary-weighted energy relative to an arbitrary constant vector.

Equations

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

theorem HCPolySupport.HighContrast.exists_euclideanBoundaryWeightedEnergyAround_le_of_pointwisePotential {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 → Vec d), Measurable F → ∀ (m : Vec d) (P : ENNReal), P ≠ ⊤ → (∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict U, euclideanBoundaryWeight U (2 * s) x * ENNReal.ofReal (vecNormSq (F x - m)) ≤ P * (∫⁻ (y : Vec d) in U, fractionalBoundarySchurKernel U s x y * fractionalGagliardoAmplitude U s F y) ^ 2) → euclideanBoundaryWeightedEnergyAround U (2 * s) F m ≤ P * C * fracSeminormSq U s F

A Schur-ready pointwise potential representation implies the normalized boundary-weighted estimate relative to the same reference vector.