High-contrast homogenization: Provider.Response.PreYoungFixedGridRows #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Cutoff-mean rows, fixed grid #
The cutoff-mean 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
{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 ≠ ⊤)
:
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 primal cutoff mean satisfies both component row estimates whenever the profile weak quantity is finite.
theorem
HCPolySupport.HighContrast.Response.FixedGrid.profile_adjoint_cutoff_mean_rows_le
{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 ≠ ⊤)
:
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 adjoint cutoff mean satisfies both component row estimates whenever the profile weak quantity is finite.