High-contrast homogenization: Provider.Response.PreYoungFixedGridComponentRows #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Cutoff-mean component rows, fixed grid #
The cutoff-mean component rows on a fixed rounded grid: the grid stays rounded at the fixed
alignment l while the generation window {s, t} moves, the aligned-cell
integrability coming from the AlignedCellsIntegrable carrier instead of the
window multiplier's carrier equality. The proof is unchanged apart from the
window bundle replaced by the carrier.
theorem
HCPolySupport.HighContrast.Response.FixedGrid.profile_primal_cutoff_mean_rows_le_of_recent_defect
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
(hstat : IsStationaryLaw P)
{l : ℤ}
{m0 q : Mat d}
(hm0 : Matrix.PosDef m0)
(hgrid : IsRoundedGrid l q)
{s t : ℤ}
(hls : l ≤ s)
(H : ℕ)
(ht : t = s + ↑H)
(hcells : AlignedCellsIntegrable P q s t)
(hblocks : ∀ (k : ℤ), l ≤ k → k ≤ t → HasFiniteAdaptedMean P q k ∧ Book.Ch02.BlockPosDef (adaptedMean P q k))
(g : Mat d)
(hg : IsSkewMat g)
(p r : Vec d)
(hweak : profilePrimalWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤)
(hdefects :
have hq := ⋯;
have X := profilePrimalCenter P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r;
have tau := profilePrimalResponseDefect P hq g hg s t p r;
have cut := adaptedPreYoungCutoff q hq t;
have child := fun (w : Fin d → ℤ) (a : CoeffSpace d) => diagonalWeakChildState hq s w (a.subSkew g hg) p r;
have parent := fun (a : CoeffSpace d) => diagonalWeakState hq t (a.subSkew g hg) p r;
ENNReal.ofReal
|avsum (alignedIndex q s t) fun (w : Fin d → ℤ) =>
(1 - volumeAverage (adaptedCellAt q s w) cut) * ∑ i : Fin d,
X.2 i * (∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (child w a)) (Sum.inl i) ∂P - ∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (parent a)) (Sum.inl i) ∂P)| ≤ ENNReal.ofReal (√(4 * tau) * profileSchurLoadFlux (profileHattedBlock g (adaptedMean P q s)) X.2) ∧ ENNReal.ofReal
|avsum (alignedIndex q s t) fun (w : Fin d → ℤ) =>
(1 - volumeAverage (adaptedCellAt q s w) cut) * ∑ i : Fin d,
X.1 i * (∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (child w a)) (Sum.inr i) ∂P - ∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (parent a)) (Sum.inr i) ∂P)| ≤ ENNReal.ofReal (√(4 * tau) * profileSchurLoadGradient (profileHattedBlock g (adaptedMean P q s)) X.1))
:
have hq := ⋯;
have X := profilePrimalCenter P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r;
have tau := profilePrimalResponseDefect P hq g hg s t p r;
have EJ :=
∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) p r ∂P;
have gain := preYoungComponentCoefficient d * 3 ^ (-↑H) * √EJ;
have cut := adaptedPreYoungCutoff q hq t;
ENNReal.ofReal |vecDot X.2 (profilePrimalCutoffMean P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) cut p r).1| ≤ ENNReal.ofReal (√(4 * tau) * profileSchurLoadFlux (profileHattedBlock g (adaptedMean P q s)) X.2) + ENNReal.ofReal gain * profilePrimalHattedEarlierRow P q g s X.1 X.2 ^ (1 / 2) ∧ ENNReal.ofReal |vecDot X.1 (profilePrimalCutoffMean P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) cut p r).2| ≤ ENNReal.ofReal (√(4 * tau) * profileSchurLoadGradient (profileHattedBlock g (adaptedMean P q s)) X.1) + ENNReal.ofReal gain * profilePrimalHattedEarlierRow P q g s X.1 X.2 ^ (1 / 2)
The recent-difference row and the physical cutoff-oscillation row give the two primal cutoff-mean component bounds.
theorem
HCPolySupport.HighContrast.Response.FixedGrid.profile_adjoint_cutoff_mean_rows_le_of_recent_defect
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
(hstat : IsStationaryLaw P)
{l : ℤ}
{m0 q : Mat d}
(hm0 : Matrix.PosDef m0)
(hgrid : IsRoundedGrid l q)
{s t : ℤ}
(hls : l ≤ s)
(H : ℕ)
(ht : t = s + ↑H)
(hcells : AlignedCellsIntegrable P q s t)
(hblocks : ∀ (k : ℤ), l ≤ k → k ≤ t → HasFiniteAdaptedMean P q k ∧ Book.Ch02.BlockPosDef (adaptedMean P q k))
(g : Mat d)
(hg : IsSkewMat g)
(p r : Vec d)
(hweak : profileAdjointWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤)
(hdefects :
have hq := ⋯;
have X := profileAdjointCenter P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r;
have tau := profileAdjointResponseDefect P hq g hg s t p r;
have cut := adaptedPreYoungCutoff q hq t;
have child := fun (w : Fin d → ℤ) (a : CoeffSpace d) => diagonalWeakChildState hq s w (a.subSkew g hg).transpose p r;
have parent := fun (a : CoeffSpace d) => diagonalWeakState hq t (a.subSkew g hg).transpose p r;
ENNReal.ofReal
|avsum (alignedIndex q s t) fun (w : Fin d → ℤ) =>
(1 - volumeAverage (adaptedCellAt q s w) cut) * ∑ i : Fin d,
X.2 i * (∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (child w a)) (Sum.inl i) ∂P - ∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (parent a)) (Sum.inl i) ∂P)| ≤ ENNReal.ofReal (√(4 * tau) * profileSchurLoadFlux (profileHattedAdjointBlock g (adaptedMean P q s)) X.2) ∧ ENNReal.ofReal
|avsum (alignedIndex q s t) fun (w : Fin d → ℤ) =>
(1 - volumeAverage (adaptedCellAt q s w) cut) * ∑ i : Fin d,
X.1 i * (∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (child w a)) (Sum.inr i) ∂P - ∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (parent a)) (Sum.inr i) ∂P)| ≤ ENNReal.ofReal (√(4 * tau) * profileSchurLoadGradient (profileHattedAdjointBlock g (adaptedMean P q s)) X.1))
:
have hq := ⋯;
have X := profileAdjointCenter P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r;
have tau := profileAdjointResponseDefect P hq g hg s t p r;
have EJ :=
∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p r ∂P;
have gain := preYoungComponentCoefficient d * 3 ^ (-↑H) * √EJ;
have cut := adaptedPreYoungCutoff q hq t;
ENNReal.ofReal |vecDot X.2 (profileAdjointCutoffMean P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) cut p r).1| ≤ ENNReal.ofReal (√(4 * tau) * profileSchurLoadFlux (profileHattedAdjointBlock g (adaptedMean P q s)) X.2) + ENNReal.ofReal gain * profileAdjointHattedEarlierRow P q g s X.1 X.2 ^ (1 / 2) ∧ ENNReal.ofReal |vecDot X.1 (profileAdjointCutoffMean P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) cut p r).2| ≤ ENNReal.ofReal (√(4 * tau) * profileSchurLoadGradient (profileHattedAdjointBlock g (adaptedMean P q s)) X.1) + ENNReal.ofReal gain * profileAdjointHattedEarlierRow P q g s X.1 X.2 ^ (1 / 2)
The transposed recent-difference row and the physical cutoff-oscillation row give the two adjoint cutoff-mean component bounds.