High-contrast homogenization: Provider.Response.PreYoungPrimalProjectedRowBound

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

Finite projected primal rows

The finite cube projections of the primal potential pairing are integrable, and their annealed absolute values obey a depth-independent bound by the all-earlier hatted row.

theorem HCPolySupport.HighContrast.Response.integrable_abs_primal_cell_pairing_of_weak {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q m0 : Mat d} (hq : Matrix.PosDef q) (hm0 : Matrix.PosDef m0) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (g : Mat d) (hg : IsSkewMat g) (p r Qcen : Vec d) (hweak : profilePrimalWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => |vecDot Qcen (blockCellAverage (adaptedCellAt q k w) (diagonalWeakState hq t (a.subSkew g hg) p r)).1|) P

Finiteness of the primal weak quantity makes every absolute potential-slot cell pairing integrable over the coefficient law.

theorem HCPolySupport.HighContrast.Response.sharp_depth_term_eq_scale_term (C R : ℝ) (s t : ℤ) (j : ℕ) : C * 3 ^ (-(t - s + ↑j)) * (2 * R) = 6 * C * 3 ^ (-(↑t - ↑s)) * (3 ^ (↑(s - ↑(j + 1)) - ↑s) * R)

The sharp cutoff decay at projection depth j is the corresponding fine-scale row weight, including the factor from the half-energy convention.

theorem HCPolySupport.HighContrast.Response.sum_sharp_depth_rows_le_scale_rows {d : ℕ} [NeZero d] (s t : ℤ) (N : ℕ) (row : ℤ → ℝ) (hrow : ∀ (k : ℤ), 0 ≤ row k) : ∑ j ∈ Finset.range N, 32 * ↑d ^ 2 * smoothTransitionProfile.derivBound * 3 ^ (-(t - s + ↑j)) * (2 * row (s - ↑(j + 1))) ≤ adaptedCutoffDerivativeCoeff d * 3 ^ (-(↑t - ↑s)) * ∑ k ∈ Finset.Icc (s - ↑N) s, 3 ^ (↑k - ↑s) * row k

Reindexing projection depths by fine scales and enlarging to a closed integer interval is absorbed by the common cutoff derivative coefficient.

theorem HCPolySupport.HighContrast.Response.aestrongly_measurable_primal_projected_oscillation {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hst : s ≤ t) (g : Mat d) (hg : IsSkewMat g) (p r Qcen : Vec d) (N : ℕ) : MeasureTheory.AEStronglyMeasurable (primalProjectedOscillation hq s t g hg p r Qcen N) P

Every finite projected primal oscillation is almost-everywhere strongly measurable under the coefficient law.