High-contrast homogenization: Provider.Response.PreYoungFixedGridDischarge

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

Unconditional pre-Young response families on a fixed rounded grid

The unconditional pre-Young response families on a fixed rounded grid: the grid is rounded once at the fixed alignment l while the generation window {s, t} moves, and the aligned-cell integrability is drawn from the coarse ellipticity e.coarse.ellipticity instead of the window multiplier, whose coupled window cannot reach an arbitrary terminal generation from a fixed alignment. No window, profile, or history premise enters: beyond the grid and window geometry the hypotheses are stationarity, Dagger, and the finite adapted means with their block positivity on the window.

theorem HCPolySupport.HighContrast.Response.FixedGrid.exists_pre_young_response_families_of_dagger_fixed_grid (d : ℕ) [NeZero d] : ∃ (Cpre : ℝ), 1 ≤ Cpre ∧ ∀ {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P], IsStationaryLaw P → ∀ {gdag : ℝ} {Edag : BlockMat d} {Psidag : ℝ → ℝ} {Kdag : ℝ} {Sdag : CoeffSpace d → ℝ}, CoarseEllipticityDagger P gdag Edag Psidag Kdag Sdag → ∀ {l : ℤ} {m0 q : Mat d}, Matrix.PosDef m0 → q = roundedGrid l m0 → ∀ (hgrid : IsRoundedGrid l q) {s t : ℤ}, l ≤ s → ∀ (H : ℕ), t = s + ↑H → (∀ (k : ℤ), l ≤ k → k ≤ t → HasFiniteAdaptedMean P q k ∧ Book.Ch02.BlockPosDef (adaptedMean P q k)) → (∀ (Cresp : ℝ), Cpre ≤ Cresp → ∀ (h0 : { h : Mat d // IsSkewMat h }) (p r : Vec d), have hq := ⋯; have X := profilePrimalCenter P hq t (fun (a : CoeffSpace d) => a.subSkew ↑h0 ⋯) p r; have tau := profilePrimalResponseDefect P hq ↑h0 ⋯ s t p r; have EJ := ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew ↑h0 ⋯).coeffOn (adaptedDomain hq t)) p r ∂P; have row := profilePrimalHattedEarlierRow P q (↑h0) s X.1 X.2; have weak := profilePrimalWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew ↑h0 ⋯) p r; have Jtilde := EJ - 1 / 2 * vecDot (fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageGradient (adaptedDomain hq t) ((a.subSkew ↑h0 ⋯).coeffOn (adaptedDomain hq t)) (centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew ↑h0 ⋯) p r) i ∂P) fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageFlux (adaptedDomain hq t) ((a.subSkew ↑h0 ⋯).coeffOn (adaptedDomain hq t)) (centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew ↑h0 ⋯) p r) i ∂P; ENNReal.ofReal |Jtilde| ≤ ENNReal.ofReal Cresp * ENNReal.ofReal √tau * (ENNReal.ofReal √tau + ENNReal.ofReal √EJ + row ^ (1 / 2)) + ENNReal.ofReal Cresp * ENNReal.ofReal (3 ^ (-↑H)) * ENNReal.ofReal √EJ * (ENNReal.ofReal √EJ + row ^ (1 / 2)) + ENNReal.ofReal Cresp * weak) ∧ ∀ (Cresp : ℝ), Cpre ≤ Cresp → ∀ (h0 : { h : Mat d // IsSkewMat h }) (p r : Vec d), have hq := ⋯; have X := profileAdjointCenter P hq t (fun (a : CoeffSpace d) => a.subSkew ↑h0 ⋯) p r; have tau := profileAdjointResponseDefect P hq ↑h0 ⋯ s t p r; have EJ := ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew ↑h0 ⋯).transpose.coeffOn (adaptedDomain hq t)) p r ∂P; have row := profileAdjointHattedEarlierRow P q (↑h0) s X.1 X.2; have weak := profileAdjointWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew ↑h0 ⋯) p r; have Jtilde := EJ - 1 / 2 * vecDot (fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageGradient (adaptedDomain hq t) ((a.subSkew ↑h0 ⋯).transpose.coeffOn (adaptedDomain hq t)) (centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew ↑h0 ⋯) p r) i ∂P) fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageFlux (adaptedDomain hq t) ((a.subSkew ↑h0 ⋯).transpose.coeffOn (adaptedDomain hq t)) (centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew ↑h0 ⋯) p r) i ∂P; ENNReal.ofReal |Jtilde| ≤ ENNReal.ofReal Cresp * ENNReal.ofReal √tau * (ENNReal.ofReal √tau + ENNReal.ofReal √EJ + row ^ (1 / 2)) + ENNReal.ofReal Cresp * ENNReal.ofReal (3 ^ (-↑H)) * ENNReal.ofReal √EJ * (ENNReal.ofReal √EJ + row ^ (1 / 2)) + ENNReal.ofReal Cresp * weak

There is a common dimension-dependent constant for the primal and adjoint compact pre-Young response families on a fixed rounded grid, with the aligned-cell integrability supplied by e.coarse.ellipticity.