High-contrast homogenization: Provider.Response.PreYoungFixedGridPrimalProjectedRows

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

Finite projected primal rows, fixed grid

Fixed-rounded-grid sibling of HCPoly.Provider.Response.PreYoungPrimalProjectedRowBound, HCPoly.Provider.Response.PreYoungPrimalFluxProjectedRowBound: 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.integrable_primal_projected_oscillation_and_integral_abs_le_scale_rows {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) (hst : s ≤ t) (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 Pcen Qcen : Vec d) (hweak : profilePrimalWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) (N : ℕ) : MeasureTheory.Integrable (primalProjectedOscillation ⋯ s t g hg p r Qcen N) P ∧ ∫ (a : CoeffSpace d), |primalProjectedOscillation ⋯ s t g hg p r Qcen N a| ∂P ≤ adaptedCutoffDerivativeCoeff d * 3 ^ (-(↑t - ↑s)) * ∑ k ∈ Finset.Icc (s - ↑N) s, 3 ^ (↑k - ↑s) * avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => profileRowCellEnergy P ⋯ k s t w (fun (a : CoeffSpace d) => a.subSkew g hg) p r * profileSchurLoadFlux (profileHattedBlock g (annealedBlock P (adaptedCellAt q k w))) Qcen

A finite projected primal oscillation is integrable, and its expected absolute value is bounded by the corresponding finite weighted row.

theorem HCPolySupport.HighContrast.Response.FixedGrid.lintegral_primal_projected_oscillation_le_row {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) (hst : s ≤ t) (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 Pcen Qcen : Vec d) (hweak : profilePrimalWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) (N : ℕ) : ∫⁻ (a : CoeffSpace d), ENNReal.ofReal |primalProjectedOscillation ⋯ s t g hg p r Qcen N a| ∂P ≤ ENNReal.ofReal (preYoungRowCoefficient d * 3 ^ (-(↑t - ↑s)) * √(∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain ⋯ t) ((a.subSkew g hg).coeffOn (adaptedDomain ⋯ t)) p r ∂P)) * profilePrimalHattedEarlierRow P q g s Pcen Qcen ^ (1 / 2)

The absolute lower integral of every finite primal projection has a common bound by the all-earlier hatted row.

theorem HCPolySupport.HighContrast.Response.FixedGrid.integrable_primal_flux_projected_oscillation_and_integral_abs_le_scale_rows {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) (hst : s ≤ t) (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 Pcen Qcen : Vec d) (hweak : profilePrimalWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) (N : ℕ) : MeasureTheory.Integrable (primalFluxProjectedOscillation ⋯ s t g hg p r Pcen N) P ∧ ∫ (a : CoeffSpace d), |primalFluxProjectedOscillation ⋯ s t g hg p r Pcen N a| ∂P ≤ adaptedCutoffDerivativeCoeff d * 3 ^ (-(↑t - ↑s)) * ∑ k ∈ Finset.Icc (s - ↑N) s, 3 ^ (↑k - ↑s) * avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => profileRowCellEnergy P ⋯ k s t w (fun (a : CoeffSpace d) => a.subSkew g hg) p r * profileSchurLoadGradient (profileHattedBlock g (annealedBlock P (adaptedCellAt q k w))) Pcen

A finite projected primal flux oscillation is integrable, and its expected absolute value is bounded by the corresponding finite weighted row.

theorem HCPolySupport.HighContrast.Response.FixedGrid.lintegral_primal_flux_projected_oscillation_le_row {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) (hst : s ≤ t) (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 Pcen Qcen : Vec d) (hweak : profilePrimalWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) (N : ℕ) : ∫⁻ (a : CoeffSpace d), ENNReal.ofReal |primalFluxProjectedOscillation ⋯ s t g hg p r Pcen N a| ∂P ≤ ENNReal.ofReal (preYoungRowCoefficient d * 3 ^ (-(↑t - ↑s)) * √(∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain ⋯ t) ((a.subSkew g hg).coeffOn (adaptedDomain ⋯ t)) p r ∂P)) * profilePrimalHattedEarlierRow P q g s Pcen Qcen ^ (1 / 2)

The absolute lower integral of every finite primal flux projection has a common bound by the all-earlier hatted row.