High-contrast homogenization: Provider.Response.PreYoungRecentDefectRows #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.Response.integral_abs_pairing_le_sqrt_two_mul_energy
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{pair energy load : CoeffSpace d → ℝ}
{annealedLoad : ℝ}
(henergy : ∀ (a : CoeffSpace d), 0 ≤ energy a)
(hload : ∀ (a : CoeffSpace d), 0 ≤ load a)
(hannealedLoad : 0 ≤ annealedLoad)
(hpoint : ∀ (a : CoeffSpace d), |pair a| ≤ √(2 * energy a) * load a)
(hmeasPair : MeasureTheory.AEStronglyMeasurable pair P)
(hintEnergy : MeasureTheory.Integrable energy P)
(hintLoadSq : MeasureTheory.Integrable (fun (a : CoeffSpace d) => load a ^ 2) P)
(hloadIntegral : ∫ (a : CoeffSpace d), load a ^ 2 ∂P = annealedLoad ^ 2)
:
A pointwise pairing bound against the square root of twice an energy passes through law-space Cauchy--Schwarz.
theorem
HCPolySupport.HighContrast.Response.integrable_child_sub_skew_readout
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
(hstat : IsStationaryLaw P)
{l s : ℤ}
{q : Mat d}
(hgrid : IsRoundedGrid l q)
(hls : l ≤ s)
(hints : HasFiniteAdaptedMean P q s)
(g : Mat d)
(hg : IsSkewMat g)
(p r : Vec d)
(w : Fin d → ℤ)
(alpha : BlockCoord d)
:
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (diagonalWeakChildState ⋯ s w (a.subSkew g hg) p r)) alpha)
P
theorem
HCPolySupport.HighContrast.Response.integrable_child_adjoint_sub_skew_readout
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
(hstat : IsStationaryLaw P)
{l s : ℤ}
{q : Mat d}
(hgrid : IsRoundedGrid l q)
(hls : l ≤ s)
(hints : HasFiniteAdaptedMean P q s)
(g : Mat d)
(hg : IsSkewMat g)
(p r : Vec d)
(w : Fin d → ℤ)
(alpha : BlockCoord d)
:
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
toFullBlockVec
(blockCellAverage (adaptedCellAt q s w) (diagonalWeakChildState ⋯ s w (a.subSkew g hg).transpose p r)) alpha)
P
theorem
HCPolySupport.HighContrast.Response.profile_primal_recent_defect_rows_le
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
(hstat : IsStationaryLaw P)
{l s t : ℤ}
{q m0 : Mat d}
(hgrid : IsRoundedGrid l q)
(hls : l ≤ s)
(hst : s ≤ t)
(hints : HasFiniteAdaptedMean P q s)
(hintt : HasFiniteAdaptedMean P q t)
(hm0 : Matrix.PosDef m0)
(g : Mat d)
(hg : IsSkewMat g)
(p r Pcen Qcen : Vec d)
(hweak : profilePrimalWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤)
:
have hq := ⋯;
have X := fun (a : CoeffSpace d) => diagonalWeakState hq t (a.subSkew g hg) p r;
have Y := fun (w : Fin d → ℤ) (a : CoeffSpace d) => diagonalWeakChildState hq s w (a.subSkew g hg) p r;
|avsum (alignedIndex q s t) fun (w : Fin d → ℤ) =>
(1 - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * ∑ i : Fin d,
Qcen i * (∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (Y w a)) (Sum.inl i) ∂P - ∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (X a)) (Sum.inl i) ∂P)| ≤ √(4 * profilePrimalResponseDefect P hq g hg s t p r) * profileSchurLoadFlux (profileHattedBlock g (adaptedMean P q s)) Qcen ∧ |avsum (alignedIndex q s t) fun (w : Fin d → ℤ) =>
(1 - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * ∑ i : Fin d,
Pcen i * (∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (Y w a)) (Sum.inr i) ∂P - ∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (X a)) (Sum.inr i) ∂P)| ≤ √(4 * profilePrimalResponseDefect P hq g hg s t p r) * profileSchurLoadGradient (profileHattedBlock g (adaptedMean P q s)) Pcen
The two literal primal recent-defect rows have the full-energy normalization dictated by the half-energy response defect.
theorem
HCPolySupport.HighContrast.Response.profile_adjoint_recent_defect_rows_le
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
(hstat : IsStationaryLaw P)
{l s t : ℤ}
{q m0 : Mat d}
(hgrid : IsRoundedGrid l q)
(hls : l ≤ s)
(hst : s ≤ t)
(hints : HasFiniteAdaptedMean P q s)
(hintt : HasFiniteAdaptedMean P q t)
(hm0 : Matrix.PosDef m0)
(g : Mat d)
(hg : IsSkewMat g)
(p r Pcen Qcen : Vec d)
(hweak : profileAdjointWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤)
:
have hq := ⋯;
have X := fun (a : CoeffSpace d) => diagonalWeakState hq t (a.subSkew g hg).transpose p r;
have Y := fun (w : Fin d → ℤ) (a : CoeffSpace d) => diagonalWeakChildState hq s w (a.subSkew g hg).transpose p r;
|avsum (alignedIndex q s t) fun (w : Fin d → ℤ) =>
(1 - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * ∑ i : Fin d,
Qcen i * (∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (Y w a)) (Sum.inl i) ∂P - ∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (X a)) (Sum.inl i) ∂P)| ≤ √(4 * profileAdjointResponseDefect P hq g hg s t p r) * profileSchurLoadFlux (profileHattedAdjointBlock g (adaptedMean P q s)) Qcen ∧ |avsum (alignedIndex q s t) fun (w : Fin d → ℤ) =>
(1 - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * ∑ i : Fin d,
Pcen i * (∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (Y w a)) (Sum.inr i) ∂P - ∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (X a)) (Sum.inr i) ∂P)| ≤ √(4 * profileAdjointResponseDefect P hq g hg s t p r) * profileSchurLoadGradient (profileHattedAdjointBlock g (adaptedMean P q s)) Pcen
The two literal adjoint recent-defect rows have the full-energy normalization dictated by the transposed half-energy response defect.