High-contrast homogenization: Provider.PolynomialHomogenization.RuledLocalizationAssembly

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

Assembly of the ruled localization provider

This module couples one ruled Whitney carrier, one buffered comparison realization, the positive Hardy row, and the print-order rate certificate. The comparison realization and its finite quantitative schedule are retained as a named selected-instance trace; no datum or Caccioppoli premise is strengthened to every carrier or every comparison family.

The numerical endpoint below is the common cap for the two realized rows. Its coefficient is selected before the stochastic exponent, and that exponent is selected before the comparison matrix, coefficient sample, and domain.

noncomputable def HCPolySupport.HighContrast.ruledScheduledTwoRowCap (d : ℕ) (hardyConstant errorCap : ENNReal) : ENNReal

The normalized duality price obtained when each of the two realized rows is bounded by the same finite error cap.

Equations

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

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

The available integrable Hardy selector supplies the exact constant consumed by the dependent assembly constructor, with no continuity or carrier premise.