High-contrast homogenization: Provider.Response.PreYoungFixedGridProjectionLimits

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

Physical projection limits, fixed grid

Fixed-rounded-grid sibling of HCPoly.Provider.Response.PreYoungPrimalPhysicalProjectionLimit, HCPoly.Provider.Response.PreYoungPrimalFluxPhysicalProjectionLimit, HCPoly.Provider.Response.PreYoungAdjointGradientPhysicalProjectionLimit, HCPoly.Provider.Response.PreYoungAdjointFluxPhysicalProjectionLimit: 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.of_real_abs_integral_primal_physical_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 ≠ ⊤) : ENNReal.ofReal |∫ (a : CoeffSpace d), primalPhysicalOscillation ⋯ s t g hg p r Qcen 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 physical primal cutoff oscillation is controlled by the earlier profile row.

theorem HCPolySupport.HighContrast.Response.FixedGrid.of_real_abs_integral_primal_flux_physical_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 ≠ ⊤) : ENNReal.ofReal |∫ (a : CoeffSpace d), primalFluxPhysicalOscillation ⋯ s t g hg p r Pcen 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 physical primal flux cutoff oscillation is controlled by the earlier profile row.

theorem HCPolySupport.HighContrast.Response.FixedGrid.of_real_abs_integral_adjoint_gradient_physical_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 : profileAdjointWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) : ENNReal.ofReal |∫ (a : CoeffSpace d), adjointGradientPhysicalOscillation ⋯ s t g hg p r Qcen a ∂P| ≤ ENNReal.ofReal (preYoungRowCoefficient d * 3 ^ (-(↑t - ↑s)) * √(∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain ⋯ t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain ⋯ t)) p r ∂P)) * profileAdjointHattedEarlierRow P q g s Pcen Qcen ^ (1 / 2)

The physical adjoint gradient cutoff oscillation is controlled by the earlier transposed profile row.

theorem HCPolySupport.HighContrast.Response.FixedGrid.of_real_abs_integral_adjoint_flux_physical_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 : profileAdjointWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) : ENNReal.ofReal |∫ (a : CoeffSpace d), adjointFluxPhysicalOscillation ⋯ s t g hg p r Pcen a ∂P| ≤ ENNReal.ofReal (preYoungRowCoefficient d * 3 ^ (-(↑t - ↑s)) * √(∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain ⋯ t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain ⋯ t)) p r ∂P)) * profileAdjointHattedEarlierRow P q g s Pcen Qcen ^ (1 / 2)

The physical adjoint flux cutoff oscillation is controlled by the earlier transposed profile row.