High-contrast homogenization: Provider.PolynomialHomogenization.RuledPairingAggregation

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

Pairing aggregation over ruled Whitney cells

The exact ruled-cell decomposition and countable Cauchy--Schwarz estimate combine the local negative and positive fractional squares. The negative row is then priced by the physical full-dual row. Exact disjointness leaves the supplied positive-row coefficient unchanged.

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

The negative fractional square of a ruled-cell-indexed field.

Equations

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

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

The physical full-dual Besov square of a ruled-cell-indexed field.

Equations

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

theorem HCPolySupport.HighContrast.ofReal_abs_volumeAverage_vecDot_le_familyCellDuality {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 : system.CellIndex → Vec d → Vec d) (G : Vec d → Vec d) (hF : MeasureTheory.MemLp (F i) 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 i x) (G x)| ≤ negativeWhitneyFamilyCellEnergy system s F i ^ (1 / 2) * ruledPositiveWhitneyCellEnergy system s G i ^ (1 / 2)

Cellwise fractional duality for a ruled family of local negative fields tested against one global positive field.

theorem HCPolySupport.HighContrast.ofReal_abs_volumeAverage_le_normalizedWhitneyRow_cauchySchwarz {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hd : 1 ≤ d) (hU : IsOpenBoundedConvexDomain U) (hUpos : 0 < MeasureTheory.volume U) (hUtop : MeasureTheory.volume U ≠ ⊤) {f : Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f U MeasureTheory.volume) (N P : system.CellIndex → ENNReal) (hcell : ∀ (i : system.CellIndex), ENNReal.ofReal |volumeAverage (system.cell i) f| ≤ N i ^ (1 / 2) * P i ^ (1 / 2)) : ENNReal.ofReal |volumeAverage U f| ≤ normalizedWhitneyRowEnergy system N ^ (1 / 2) * normalizedWhitneyRowEnergy system P ^ (1 / 2)

Normalized constant-one Cauchy--Schwarz aggregation over the ruled Whitney decomposition.

theorem HCPolySupport.HighContrast.normalizedNegativeWhitneyFamilyRow_le_fullDualRow {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} {rho Rad s : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hs : 0 < s) (hsHalf : s < 1 / 2) (F : system.CellIndex → Vec d → Vec d) (hF : ∀ (i : system.CellIndex), MemVectorL2 (system.cell i) (F i)) : normalizedWhitneyRowEnergy system (negativeWhitneyFamilyCellEnergy system s F) ≤ fractionalDualToBesovConstant d ^ 2 * normalizedWhitneyRowEnergy system (physicalFullDualWhitneyFamilyCellEnergy system s F)

The complete ruled negative row is bounded by the physical full-dual row with the finite dimension-only density coefficient.

theorem HCPolySupport.HighContrast.ofReal_abs_volumeAverage_vecDot_le_fullDualWhitneyRow_mul_hs {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} {rho Rad s : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hU : IsOpenBoundedConvexDomain U) (hUpos : 0 < MeasureTheory.volume U) (hUtop : MeasureTheory.volume U ≠ ⊤) (hs : 0 < s) (hsHalf : s < 1 / 2) (F : system.CellIndex → Vec d → Vec d) (G : Vec d → Vec d) (f : Vec d → ℝ) (hf : MeasureTheory.IntegrableOn f U MeasureTheory.volume) (hpair : ∀ (i : system.CellIndex), volumeAverage (system.cell i) f = volumeAverage (system.cell i) fun (x : Vec d) => vecDot (F i x) (G x)) (hF : ∀ (i : system.CellIndex), MeasureTheory.MemLp (F i) 2 (MeasureTheory.volume.restrict (system.cell i))) (hG : ∀ (i : system.CellIndex), MeasureTheory.Integrable G (MeasureTheory.volume.restrict (system.cell i))) (hGfinite : ∀ (i : system.CellIndex), hsNormSq (system.cell i) s G ≠ ⊤) {C : ENNReal} (hHardy : normalizedWhitneyRowEnergy system (ruledPositiveWhitneyCellEnergy system s G) ≤ C * hsNormSq U s G) : ENNReal.ofReal |volumeAverage U f| ≤ (fractionalDualToBesovConstant d ^ 2 * normalizedWhitneyRowEnergy system (physicalFullDualWhitneyFamilyCellEnergy system s F)) ^ (1 / 2) * (C * hsNormSq U s G) ^ (1 / 2)

The ruled physical full-dual negative row and a supplied positive Hardy row control the normalized domain pairing. Exact disjointness preserves the Hardy coefficient C without an overlap multiplier.