Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.ConvexBoundaryWeightedEnergy

High-contrast homogenization: Provider.PolynomialHomogenization.ConvexBoundaryWeightedEnergy #

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

Centering the boundary-weighted energy #

The boundary-weighted L² energy is split into its domain-centered part and the contribution of the domain average. The latter is controlled by the negative boundary-distance moment on a ball-sandwiched convex domain.

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

The normalized boundary-distance-weighted energy of a vector field.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.euclideanBoundaryWeightedCenteredEnergy {d : ℕ} (U : Set (Vec d)) (p : ℝ) (F : Vec d → Vec d) :
    ENNReal

    The normalized boundary-weighted energy after subtracting the domain average.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.HighContrast.euclideanBoundaryWeightedEnergy_le_centered_add_mean {d : ℕ} {U : Set (Vec d)} {F : Vec d → Vec d} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict U)) (p : ℝ) :
      euclideanBoundaryWeightedEnergy U p F ≤ 2 * euclideanBoundaryWeightedCenteredEnergy U p F + 2 * ENNReal.ofReal (vecNormSq (volumeAverageVec U F)) * euclideanBoundaryWeightMoment U p

      Centering separates the only genuinely analytic Hardy--Poincare term from a spatially constant boundary moment.

      source
      theorem HCPolySupport.HighContrast.euclideanBoundaryWeightedEnergy_le_centered_add_explicitMean {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)) {F : Vec d → Vec d} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict U)) :
      euclideanBoundaryWeightedEnergy U (2 * s) F ≤ 2 * euclideanBoundaryWeightedCenteredEnergy U (2 * s) F + 2 * ENNReal.ofReal (vecNormSq (volumeAverageVec U F)) * ENNReal.ofReal ((↑d / rho) ^ (2 * s) / (1 - 2 * s))

      The mean part of the fractional boundary-weighted energy has an explicit ball-sandwich bound.