High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.RowSupply.CdualConditionalTerminalProducer
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Terminal producer conditional on domain duality #
The quantitative flux row is complete. The only remaining analytic input in this terminal adapter is the ruled arbitrary-domain flux-defect duality.
theorem
HCPolySupport.HighContrast.RowSupply.negSobolevNorm_le_of_rowConvertedFluxCap
{d : ℕ}
[NeZero d]
{U : Set (Vec d)}
{rho Rad s : ℝ}
(system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad)
(hU : IsOpenBoundedConvexDomain U)
(hUnonempty : U.Nonempty)
(hs : 0 < s)
(hsHalf : s < 1 / 2)
(F : Vec d → Vec d)
(hF : MemVectorL2 U F)
{cap hardyConstant : ENNReal}
(hRow :
normalizedWhitneyRowEnergy system (physicalFullDualWhitneyFamilyCellEnergy system s fun (x : system.CellIndex) => F) ≤ cap)
(hHardy :
∀ (G : Vec d → Vec d),
MeasureTheory.Integrable G (MeasureTheory.volume.restrict U) →
PrintFaithfulPositiveTestRow system s G hardyConstant)
:
negSobolevNorm U s F ≤ (fractionalDualToBesovConstant d ^ 2 * cap) ^ (1 / 2) * hardyConstant ^ (1 / 2)
A finite printed full-dual flux row controls its compact-test negative Sobolev norm through the pure Hardy row.
theorem
HCPolySupport.HighContrast.RowSupply.rowConvertedTerminalBound_of_domainDuality
{d : ℕ}
[NeZero d]
{U : Set (Vec d)}
{rho Rad s epsilon Xval outputFactor : ℝ}
(system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad)
(hU : IsOpenBoundedConvexDomain U)
(hUnonempty : U.Nonempty)
(hs : 0 < s)
(hsHalf : s < 1 / 2)
(aPhysical : CoeffField d)
(u h : H1Function U)
(hF : MemVectorL2 U fun (x : Vec d) => matVecMul (aPhysical x - 1) (u.grad x))
{capFlux hardyConstant boundaryEnergy : ENNReal}
{Cdual : ℝ}
(hRow :
normalizedWhitneyRowEnergy system
(physicalFullDualWhitneyFamilyCellEnergy system s
(ruledPhysicalFluxDefectOnCell system aPhysical (fun (x : system.CellIndex) => identityConstantCoeffMatrix d)
u)) ≤ capFlux)
(hHardy :
∀ (G : Vec d → Vec d),
MeasureTheory.Integrable G (MeasureTheory.volume.restrict U) →
PrintFaithfulPositiveTestRow system s G hardyConstant)
(hDual : PrintFaithfulDomainFluxDefectDuality U s aPhysical u h Cdual)
{C₀ : ℝ → ℝ → ℝ → ℝ}
{g kappaRate : ℝ}
(hRate :
RowConvertedFluxScheduledRateAtWitness d C₀ g kappaRate Cdual capFlux hardyConstant boundaryEnergy s rho Rad epsilon
Xval outputFactor)
:
Once the converted flux rate is supplied, the domain comparison is conditional only on the printed arbitrary-domain duality statement.