Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.BufferToCell.PositiveBesovContinuousComparison

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.BufferToCell.PositiveBesovContinuousComparison

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

Local positive Besov comparison #

The Chapter-3 positive Besov norm is controlled by the continuous Euclidean fractional square. The explicit factor is the square of the cube side length; it is retained here so that the ruled carrier can price it by its outer radius.

source
noncomputable def HCPolySupport.HighContrast.BufferToCell.normalizedDomainMeasure {d : ℕ} (V : Set (Vec d)) :
MeasureTheory.Measure (Vec d)

Restricted volume on V, scaled by the inverse of its total volume.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.BufferToCell.ofReal_vecNormSq_volumeAverageVec_le_eVolumeAverage {d : ℕ} {V : Set (Vec d)} (hVpos : 0 < MeasureTheory.volume V) (hVtop : MeasureTheory.volume V ≠ ⊤) {F : Vec d → Vec d} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict V)) :
    ENNReal.ofReal (vecNormSq (volumeAverageVec V F)) ≤ eVolumeAverage V fun (x : Vec d) => ENNReal.ofReal (vecNormSq (F x))
    source
    theorem HCPolySupport.HighContrast.BufferToCell.ofReal_vecNormSq_cubeAverageVec_le_eVolumeAverage {d : ℕ} (Q : TriadicCube d) {F : Vec d → Vec d} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict (openCubeSet Q))) :
    ENNReal.ofReal (vecNormSq (cubeAverageVec Q F)) ≤ eVolumeAverage (openCubeSet Q) fun (x : Vec d) => ENNReal.ofReal (vecNormSq (F x))
    source
    noncomputable def HCPolySupport.HighContrast.BufferToCell.positiveBesovContinuousComparisonConstant (d : ℕ) :
    ℝ

    The dimension-only comparison coefficient between the Chapter-3 positive Besov norm and the continuous Euclidean fractional square.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.HighContrast.BufferToCell.positiveBesovContinuousComparisonConstant_pos (d : ℕ) :
      0 < positiveBesovContinuousComparisonConstant d
      source
      theorem HCPolySupport.HighContrast.BufferToCell.positiveBesovNorm_sq_le_continuousFractionalSquare {d : ℕ} [NeZero d] (Q : TriadicCube d) (sF : ↑FractionalOrder) (F : Vec d → Vec d) (hBesov : Book.Ch03.ForceBesovRegularity Q (↑sF) F) (hFcube : MemVectorL2 (openCubeSet Q) F) :
      ENNReal.ofReal (Book.Ch03.scaleNormalizedPositiveBesovVectorNormTwo Q (↑sF) F) ^ 2 ≤ ENNReal.ofReal (positiveBesovContinuousComparisonConstant d) * ENNReal.ofReal (cubeScaleFactor Q ^ (2 * ↑sF)) * hsNormSq (openCubeSet Q) (↑sF) F

      A local Chapter-3 positive Besov square is bounded by the Euclidean fractional square, with the exact side-length factor exposed.