High-contrast homogenization: Provider.PolynomialHomogenization.RuledWhitneyCellDuality

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

noncomputable def HCPolySupport.HighContrast.scaleWeight {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (s : ℝ) (i : system.CellIndex) : ENNReal

The inverse fractional side-length weight used internally by the ruled one-cell duality calculation.

Equations

• HCPolySupport.HighContrast.scaleWeight system s i = ENNReal.ofReal ((3 ^ system.scale i) ^ (-2 * s))

noncomputable def HCPolySupport.HighContrast.positiveWhitneyCellEnergy {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (s : ℝ) (F : Vec d → Vec d) (i : system.CellIndex) : ENNReal

The expanded positive fractional square used internally by the ruled one-cell duality calculation.

Equations

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

theorem HCPolySupport.HighContrast.hsNormSq_whitneyCell_eq_positiveWhitneyCellEnergy {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} {rho Rad s : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i : system.CellIndex) {F : Vec d → Vec d} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict (system.cell i))) (hs : 0 ≤ s) : hsNormSq (system.cell i) s F = positiveWhitneyCellEnergy system s F i

On a Whitney cell, the expanded positive square is exactly the normalized fractional Sobolev norm square.

noncomputable def HCPolySupport.HighContrast.negativeWhitneyCellEnergy {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (s : ℝ) (F : Vec d → Vec d) (i : system.CellIndex) : ENNReal

The negative square used in the Whitney-row Cauchy--Schwarz estimate.

Equations

• HCPolySupport.HighContrast.negativeWhitneyCellEnergy system s F i = HCPolySupport.HighContrast.negSobolevNorm (system.cell i) s F ^ 2

theorem HCPolySupport.HighContrast.ofReal_abs_volumeAverage_vecDot_le_cellDuality {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} {rho Rad s : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i : system.CellIndex) (hs : 0 < s) (hsHalf : s < 1 / 2) (F G : Vec d → Vec d) (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (system.cell i))) (hG : MeasureTheory.Integrable G (MeasureTheory.volume.restrict (system.cell i))) (hGfinite : hsNormSq (system.cell i) s G ≠ ⊤) : ENNReal.ofReal |volumeAverage (system.cell i) fun (x : Vec d) => vecDot (F x) (G x)| ≤ negativeWhitneyCellEnergy system s F i ^ (1 / 2) * positiveWhitneyCellEnergy system s G i ^ (1 / 2)

Below the trace threshold, the normalized pairing on one Whitney cell is bounded by its negative and positive fractional squares.