High-contrast homogenization: Provider.Recurrence.RecurrenceAssembly

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

p.fixed.geometry.parent.child.recurrence

The fixed-grid recurrence is assembled here from the estimates of the section. On one deterministic rounded adapted grid q of alignment ℓ, at a child scale j ≥ ℓ and a parent scale p = j + h above it, the parent cell is partitioned by 3^{dh} aligned children; write G_hat for the average of the responses over those children, E_j and E_p for the two adapted means and Δ = Δ_{j,p}^q for the determinant increment.

Four displays are composed.

The averaging step. The centred average G_hat - E_j, normalized by the child mean, has mixed norm at most C(d,Q) 3^{-hd/2} times the child moment v_j^q; this is l.fixed.geometry.matrix.averaging read at the aligned subdivision, whose cardinality 3^{dh} supplies the printed gain.

The transport of the normalization. The mean order E_p ≤ E_j and the ideal property of the Schatten norm carry that estimate from the child normalization to the parent one, at the cost of (2d)^{1/Q}e^{Δ}.

The positive gap. Pathwise 0 ≤ 𝐀_p ≤ G_hat, so the normalized excess D = (G_hat - 𝐀_p)^~ is positive with mean B = P_{j,p}^q - I; the determinant transport bounds the spectral size of P_{j,p}^q by e^{Δ} and its trace gap by e^{Δ} - 1. The positive-gap estimate then bounds the parent moment by C(y + Φ_Q(Δ)), where y is the transported mixed norm of the centred average.

The gain. Substituting the transported bound for y produces the printed contraction: a geometric factor 3^{-hd/2}e^{Δ} on the child moment plus the increment's own gain Φ_Q(Δ), both carrying one constant C_rec(d, Q).

The mixed norms are ℝ≥0∞-valued, and the passage to the real inequalities the positive-gap estimate is stated in is made on the finiteness hypotheses the proposition carries. The exponent Q is an even integer, which is what makes the Schatten size a continuous function of the entries: the inner power Q/2 of |H|_{S_Q} = (tr((H²)^{Q/2}))^{1/Q} is then an integer, the functional calculus collapses to a matrix power and the trace is a polynomial. That is the content of the opening section.

Measurability of the Schatten size at an even exponent

theorem HCPolySupport.HighContrast.Recurrence.aestronglyMeasurable_entry_pow {n : Type u_1} [Fintype n] [DecidableEq n] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {F : Ω → Matrix n n ℝ} (h : ∀ (i j : n), MeasureTheory.AEStronglyMeasurable (fun (a : Ω) => F a i j) μ) (k : ℕ) (i j : n) : MeasureTheory.AEStronglyMeasurable (fun (a : Ω) => (F a ^ k) i j) μ

The entries of a matrix power are polynomials in the entries.

theorem HCPolySupport.HighContrast.Recurrence.aestronglyMeasurable_entry_conj {n : Type u_1} [Fintype n] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (S : Matrix n n ℝ) {F : Ω → Matrix n n ℝ} (h : ∀ (i j : n), MeasureTheory.AEStronglyMeasurable (fun (a : Ω) => F a i j) μ) (i j : n) : MeasureTheory.AEStronglyMeasurable (fun (a : Ω) => (S * F a * S) i j) μ

The entries of a two-sided constant congruence are linear in the entries.

theorem HCPolySupport.HighContrast.Recurrence.aestronglyMeasurable_entry_normalizedBlock_blockSub {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {X Y : CoeffSpace d → BlockMat d} (F : BlockMat d) (hX : ∀ (α β : BlockCoord d), MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => toFullBlockMat (X a) α β) P) (hY : ∀ (α β : BlockCoord d), MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => toFullBlockMat (Y a) α β) P) (α β : BlockCoord d) : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (blockSub (X a) (Y a)) F) α β) P

The entries of a normalized difference of two random doubled blocks are measurable as soon as the entries of the two blocks are: normalization and subtraction are a fixed real-linear map of the entries.

theorem HCPolySupport.HighContrast.Recurrence.aestronglyMeasurable_blockTrace {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {W : CoeffSpace d → BlockMat d} (hW : ∀ (α β : BlockCoord d), MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => toFullBlockMat (W a) α β) P) : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => blockTrace (W a)) P

The trace of a random doubled block is measurable as soon as its entries are.

theorem HCPolySupport.HighContrast.Recurrence.trace_cfc_rpow_eq_trace_pow {d : ℕ} {A : FullBlockMat d} (hA : IsSelfAdjoint A) {Q : ℕ} (hQ : Even Q) : (cfc (fun (x : ℝ) => x ^ (↑Q / 2)) A).trace = Matrix.trace (A ^ (Q / 2))

At an even natural exponent the Schatten trace of a self-adjoint matrix is the trace of a matrix power: the spectral power x ↦ x^{Q/2} is then a natural power, and the functional calculus of a natural power is that power.

theorem HCPolySupport.HighContrast.Recurrence.schattenNorm_natCast_eq {d : ℕ} {H : BlockMat d} (hH : IsSymmetricBlockMat H) {Q : ℕ} (hQ : Even Q) : schattenNorm (↑Q) H = ((toFullBlockMat H * toFullBlockMat H) ^ (Q / 2)).trace ^ (↑Q)⁻¹

The Schatten size at an even exponent is an algebraic function of the entries: |H|_{S_Q} = (tr((H²)^{Q/2}))^{1/Q} with Q/2 an integer power.

theorem HCPolySupport.HighContrast.Recurrence.aestronglyMeasurable_schattenNorm {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {H : CoeffSpace d → BlockMat d} (hH : ∀ (a : CoeffSpace d), IsSymmetricBlockMat (H a)) {Q : ℕ} (hQeven : Even Q) (hmeas : ∀ (α β : BlockCoord d), MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => toFullBlockMat (H a) α β) P) : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => schattenNorm (↑Q) (H a)) P

The Schatten size of a random symmetric doubled block is measurable at an even exponent, with no hypothesis beyond measurability of the entries: the Schatten trace is then a polynomial in them and the Q-th root is continuous.

The recurrence