High-contrast homogenization: Provider.PolynomialHomogenization.RuledHardyPositiveRow

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

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

A private byte-faithful copy of the inverse fractional scale weight from RuledWhitneyCellDuality. It is repeated here because that module keeps its one-cell implementation adapters private.

Equations

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

noncomputable def HCPolySupport.HighContrast.ruledPositiveWhitneyCellEnergy {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 shared by the ruled Hardy row and its pairing consumer. Its body is byte-faithful to the private one-cell adapter in RuledWhitneyCellDuality.

Equations

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

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

The inverse-scale local L² contribution over the ruled Whitney cells.

Equations

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

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

The normalized same-cell Gagliardo contribution over the ruled cells.

Equations

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

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

The complete positive fractional energy over the ruled Whitney cells.

Equations

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

theorem HCPolySupport.HighContrast.volume_mul_positiveWhitneyCellEnergy {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (s : ℝ) (F : Vec d → Vec d) (i : system.CellIndex) : MeasureTheory.volume (system.cell i) * ruledPositiveWhitneyCellEnergy system s F i = (ruledScaleWeight system s i * ∫⁻ (x : Vec d) in system.cell i, ENNReal.ofReal (vecNormSq (F x))) + ∫⁻ (z : Vec d × Vec d) in system.cell i ×ˢ system.cell i, whitneyRowFractionalKernel s F z ∂MeasureTheory.volume.prod MeasureTheory.volume

Multiplying one expanded ruled-cell square by its volume recovers its two raw positive-row contributions.

theorem HCPolySupport.HighContrast.rawWhitneyRowEnergy_positive_eq_volume_mul_ruledPositiveRowEnergy {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hUpos : 0 < MeasureTheory.volume U) (hUtop : MeasureTheory.volume U ≠ ⊤) (s : ℝ) (F : Vec d → Vec d) : rawWhitneyRowEnergy system (ruledPositiveWhitneyCellEnergy system s F) = MeasureTheory.volume U * ruledPositiveRowEnergy system s F

The raw row of expanded ruled-cell squares is the domain volume times the normalized ruled positive-row energy.

theorem HCPolySupport.HighContrast.normalizedWhitneyRowEnergy_positive_eq_ruledPositiveRowEnergy {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hUpos : 0 < MeasureTheory.volume U) (hUtop : MeasureTheory.volume U ≠ ⊤) (s : ℝ) (F : Vec d → Vec d) : normalizedWhitneyRowEnergy system (ruledPositiveWhitneyCellEnergy system s F) = ruledPositiveRowEnergy system s F

The normalized row of expanded ruled-cell squares is exactly the ruled positive-row energy.

theorem HCPolySupport.HighContrast.ruledPositiveRowGagliardoEnergy_le_fracSeminormSq {d : ℕ} {U : Set (Vec d)} (hUpos : 0 < MeasureTheory.volume U) (hUtop : MeasureTheory.volume U ≠ ⊤) {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) {F : Vec d → Vec d} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict U)) {s : ℝ} (hs : 0 ≤ s) : ruledPositiveRowGagliardoEnergy system s F ≤ fracSeminormSq U s F

Exact disjointness bounds the ruled same-cell Gagliardo row by one global fractional seminorm, with constant one.

theorem HCPolySupport.HighContrast.euclideanBoundaryDistance_lt_ruledScaleFactor {d : ℕ} [NeZero d] {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hU : IsOpen U) (i : system.CellIndex) {x : Vec d} (hx : x ∈ system.cell i) : euclideanBoundaryDistance U x < 41 * √↑d * 3 ^ system.scale i

The new ruled buffer gives the factor-41 upper comparison between Euclidean boundary distance and the selected cell scale.

noncomputable def HCPolySupport.HighContrast.ruledBoundaryScaleFactor (d : ℕ) (s : ℝ) : ENNReal

The extended nonnegative real factor (41 * Real.sqrt d) ^ (2 * s) used to compare ruled cell-scale weights with boundary weights.

Equations

• HCPolySupport.HighContrast.ruledBoundaryScaleFactor d s = ENNReal.ofReal ((41 * √↑d) ^ (2 * s))

theorem HCPolySupport.HighContrast.exists_normalizedRuledPositiveWhitneyRowHsConstant {d : ℕ} (hd : 1 ≤ d) {rho Rad s : ℝ} (hrho : 0 < rho) (hRad : 0 < Rad) (hs : 0 < s) (hsHalf : s < 1 / 2) : ∃ (C : ENNReal), C ≠ ⊤ ∧ ∀ (U : Set (Vec d)), IsOpenBoundedConvexDomain U → HasBallSandwich U rho Rad → ∀ (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (G : Vec d → Vec d), MeasureTheory.Integrable G (MeasureTheory.volume.restrict U) → normalizedWhitneyRowEnergy system (ruledPositiveWhitneyCellEnergy system s G) ≤ C * hsNormSq U s G

For fixed dimension, fractional order, and sandwich radii, one finite coefficient controls the normalized expanded positive row of every ruled Whitney system by the domain fractional norm square.