High-contrast homogenization: Provider.PolynomialHomogenization.FractionalGagliardoSquareFunction

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

The global fractional Gagliardo square function

noncomputable def HCPolySupport.HighContrast.fractionalGagliardoSquareFunction {d : ℕ} (U : Set (Vec d)) (s : ℝ) (F : Vec d → Vec d) (x : Vec d) : ENNReal

The unnormalized pointwise fractional energy in the second variable.

Equations

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

noncomputable def HCPolySupport.HighContrast.fractionalGagliardoAmplitude {d : ℕ} (U : Set (Vec d)) (s : ℝ) (F : Vec d → Vec d) (x : Vec d) : ENNReal

The square root of the pointwise fractional energy.

Equations

• HCPolySupport.HighContrast.fractionalGagliardoAmplitude U s F x = HCPolySupport.HighContrast.fractionalGagliardoSquareFunction U s F x ^ (1 / 2)

theorem HCPolySupport.HighContrast.measurable_fractionalGagliardoSquareFunction {d : ℕ} {U : Set (Vec d)} {s : ℝ} {F : Vec d → Vec d} (hF : Measurable F) : Measurable (fractionalGagliardoSquareFunction U s F)

theorem HCPolySupport.HighContrast.measurable_fractionalGagliardoAmplitude {d : ℕ} {U : Set (Vec d)} {s : ℝ} {F : Vec d → Vec d} (hF : Measurable F) : Measurable (fractionalGagliardoAmplitude U s F)

theorem HCPolySupport.HighContrast.fractionalGagliardoAmplitude_rpow_two {d : ℕ} (U : Set (Vec d)) (s : ℝ) (F : Vec d → Vec d) (x : Vec d) : fractionalGagliardoAmplitude U s F x ^ 2 = fractionalGagliardoSquareFunction U s F x

theorem HCPolySupport.HighContrast.setLIntegral_fractionalGagliardoAmplitude_rpow_two {d : ℕ} (U : Set (Vec d)) (s : ℝ) (F : Vec d → Vec d) : ∫⁻ (x : Vec d) in U, fractionalGagliardoAmplitude U s F x ^ 2 = ∫⁻ (x : Vec d) (y : Vec d) in U, ENNReal.ofReal (vecNormSq (F x - F y) / euclideanDist x y ^ (↑d + 2 * s))

The squared amplitude integrates to the raw regional fractional energy.

theorem HCPolySupport.HighContrast.setLIntegral_fractionalGagliardoAmplitude_rpow_two_eq {d : ℕ} {U : Set (Vec d)} (hUpos : 0 < MeasureTheory.volume U) (hUtop : MeasureTheory.volume U ≠ ⊤) (s : ℝ) (F : Vec d → Vec d) : ∫⁻ (x : Vec d) in U, fractionalGagliardoAmplitude U s F x ^ 2 = MeasureTheory.volume U * fracSeminormSq U s F

On a positive finite-volume domain, the squared amplitude is the volume times the normalized fractional seminorm.