High-contrast homogenization: Entry.Response.Kernel.BesovScaleSummationToolkit

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

The Besov seminorm's scale toolkit and the cell-average energy bound

The all-scale maximum ℳ = sup_{k ≤ t} 3^{-ρ(t-k)} max_z |(·)_+| of p.response.transfer dominates the normalized spectral defect of every triadic cell at every depth, and this file records that a pathwise response dominated by 1 + ℳ is integrable whenever ℳ's Q-th moment is, and that the pathwise response J is measurable in the sample for both recentred coefficients. It bounds the scale-average (Besov) seminorm [·] of AK.HC (2.130), and its square, by any geometrically growing per-scale majorant A · 3^{ρ n} with ρ < 1, and shows the corresponding series is summable. It proves the exact partition-averaging identity - the normalized sum of the averages of an integrable function over the depth-n triadic subcells of an adapted cell equals the average over the parent cell - and the cell-average half of AK.HC (2.15): the doubled cell average of a b-harmonic field on a cell V is controlled by the pathwise symmetric energy of the field, via the variational (Fenchel) inequality together with the canonical Cauchy-Schwarz bound.

Integrability of the all-scale envelope times the response

The all-scale maximum ℳ = sup_{k <= t} 3^{-ρ(t-k)} max_z |(...)_+| of p.response.transfer dominates the normalized spectral defect of every triadic cell at every depth, and the response estimate e.response.weak.estimate controls its Q-th moment. This file records the elementary consequence used when the envelope multiplies a pathwise response: if ℳ ^ Q is P-integrable with 2 ≤ Q and the response J is square integrable, then (1 + ℳ) J is P-integrable.

Because P is a probability measure and ℳ ≥ 0, the pointwise bound ℳ ^ 2 ≤ 1 + ℳ ^ Q (split at ℳ = 1) makes ℳ square integrable. The product (1 + ℳ) J = J + ℳ J is then a sum of integrable functions: J is integrable as an L² function on a finite measure, and ℳ J is the product of two L² functions (Hölder with conjugate exponents 2 and 2). The pathwise response is that of AK.HC (2.15).

theorem HCPolySupport.HighContrast.Multiscale.integrable_one_add_respAllScaleMax_mul_respJ {d : ℕ} (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (jStar : ℕ) (F : BlockMat d) (t : ℤ) (p q' : Vec d) (hMmeas : MeasureTheory.AEStronglyMeasurable (respAllScaleMax P γ jStar F t) P) (hMint : MeasureTheory.Integrable (fun (a : CoeffSpace d) => respAllScaleMax P γ jStar F t a ^ bigQ d γ) P) (hQ : 2 ≤ bigQ d γ) (hJsq : MeasureTheory.Integrable (fun (a : CoeffSpace d) => respJ (respGrid jStar F) t p q' (respCoeffMinus F a) ^ 2) P) (hJmeas : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => respJ (respGrid jStar F) t p q' (respCoeffMinus F a)) P) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => (1 + respAllScaleMax P γ jStar F t a) * respJ (respGrid jStar F) t p q' (respCoeffMinus F a)) P

Integrability of the all-scale envelope times the recentred response. For a probability law P, the all-scale maximum ℳ of p.response.transfer with Q-th moment integrable, 2 ≤ Q, multiplies the pathwise recentred response J(U_t; a_-, p, q') of AK.HC (2.15) into a P-integrable function: (1 + ℳ) J is integrable whenever ℳ is measurable and J ^ 2 is integrable and measurable.

theorem HCPolySupport.HighContrast.Multiscale.integrable_one_add_respAllScaleMax_mul_respJPlus {d : ℕ} (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (jStar : ℕ) (F : BlockMat d) (t : ℤ) (p q' : Vec d) (hMmeas : MeasureTheory.AEStronglyMeasurable (respAllScaleMax P γ jStar F t) P) (hMint : MeasureTheory.Integrable (fun (a : CoeffSpace d) => respAllScaleMax P γ jStar F t a ^ bigQ d γ) P) (hQ : 2 ≤ bigQ d γ) (hJsq : MeasureTheory.Integrable (fun (a : CoeffSpace d) => respJ (respGrid jStar F) t p q' (respCoeffPlus F a) ^ 2) P) (hJmeas : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => respJ (respGrid jStar F) t p q' (respCoeffPlus F a)) P) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => (1 + respAllScaleMax P γ jStar F t a) * respJ (respGrid jStar F) t p q' (respCoeffPlus F a)) P

Integrability of the all-scale envelope times the adjoint recentred response. The adjoint twin of integrable_one_add_respAllScaleMax_mul_respJ: the same probability-law argument applies with the pathwise adjoint recentred response J(U_t; a_+, p, q') of AK.HC (2.15) in place of J(U_t; a_-, p, q'), so (1 + ℳ) J is P-integrable under the same envelope-moment, measurability and square-integrability hypotheses.

The unweighted quadratic readout of the canonical cutoff pairing

The cutoff pairing of e.response.cutoff.estimate expands into one quadratic term and three linear terms (AK.HC Lemma A.1, (A.4)). CanonicalCutoffPairingMeasurability treats the three linear terms, and the quadratic term reduces to the cutoff-weighted block self-pairing of the canonical optimizer state.

This file treats the unweighted quadratic readout, the full-cell energy of the canonical optimizer,

a ↦ volumeAverage (adaptedCell q t) (fun x => vecDot Z(a,x).1 Z(a,x).2),

where Z(a,·) is the canonical optimizer state. The flux slot of that state is the recentred coefficient applied to its gradient slot, so the integrand is the a-energy density ⟨∇v, a ∇v⟩ of the canonical maximizer. The full-cell average of that density is the doubled maximizer energy, which is twice the pathwise response J(adaptedCell q t, p, r) of the recentred coefficient. The pathwise response is an explicit block quadratic of the coarse block, hence a measurable function of the sample, so the unweighted quadratic readout is measurable in the sample with no hypothesis beyond the cutoff class data. This is the φ = 1 case of the quadratic term of the expansion.

The genuinely cutoff-weighted readout is local and is not the full-cell energy; its measurability is the block self-pairing statement of the canonical optimizer state.

Measurability of the recentred pathwise responses

theorem HCPolySupport.HighContrast.Multiscale.measurable_respJ_respCoeffMinus {d : ℕ} [NeZero d] (q : Mat d) (hq : IsUnit q) (t : ℤ) (F : BlockMat d) (p r : Vec d) : Measurable fun (a : CoeffSpace d) => respJ q t p r (respCoeffMinus F a)

The recentred minus pathwise response on an adapted cell is measurable in the sample. It is the explicit block quadratic of the recentred coarse block (AK.HC (2.15)), whose flattened entries are measurable.

theorem HCPolySupport.HighContrast.Multiscale.measurable_respJ_respCoeffPlus {d : ℕ} [NeZero d] (q : Mat d) (hq : IsUnit q) (t : ℤ) (F : BlockMat d) (p r : Vec d) : Measurable fun (a : CoeffSpace d) => respJ q t p r (respCoeffPlus F a)

The recentred plus pathwise response on an adapted cell is measurable in the sample. It is the explicit block quadratic of the adjoint recentred coarse block, whose flattened entries are measurable.

The full-cell quadratic readout as twice the pathwise response

The unweighted quadratic readouts as pathwise responses

Measurability of the unweighted quadratic readouts

HC bridge III: the scale-weighted summation of the seminorm (AK.HC (2.130))

The scale-average seminorm of AK.HC (2.130) is a series of per-scale averages. The preceding bridge ScaleAverageSeminorm bounds it against the constant per-scale majorant cellMeanSq. Here the per-scale majorant is allowed to grow geometrically, A * 3 ^ (ρ * n) with ρ < 1, which is the shape produced by the multiscale coarse-block envelope. The chain is the same three steps: a termwise bound against the scale majorant, summability by comparison with a geometric series, and the resulting bound on besovSeminorm.

theorem HCPolySupport.HighContrast.Multiscale.besov_term_le_of_scale_bound {d : ℕ} (t : ℤ) (ρ A : ℝ) (hρ : ρ < 1) (hρ0 : 0 ≤ ρ) (hA : 0 ≤ A) (avg : ℕ → (Fin d → ℤ) → BlockVec d) (h : ∀ (n : ℕ), (↑(triadicIndexBox d n).card)⁻¹ * ∑ w ∈ triadicIndexBox d n, blockVecDot (avg n w) (avg n w) ≤ A * 3 ^ (ρ * ↑n)) (n : ℕ) : 3 ^ ((↑t - ↑n) / 2) * √((↑(triadicIndexBox d n).card)⁻¹ * ∑ w ∈ triadicIndexBox d n, blockVecDot (avg n w) (avg n w)) ≤ 3 ^ (↑t / 2) * √A * (3 ^ ((ρ - 1) / 2)) ^ n

Termwise bound for the scale-average seminorm against a geometrically growing per-scale majorant. If the squared average at depth n is at most A * 3 ^ (ρ * n) with ρ < 1, then the weighted n-th summand of the seminorm of AK.HC (2.130) is at most 3 ^ (t / 2) * sqrt A * (3 ^ ((ρ - 1) / 2)) ^ n, i.e. the scale weight and the growing majorant combine into the geometric ratio 3 ^ ((ρ - 1) / 2) < 1.

theorem HCPolySupport.HighContrast.Multiscale.summable_besov_of_scale_bound {d : ℕ} (t : ℤ) (ρ A : ℝ) (hρ : ρ < 1) (hρ0 : 0 ≤ ρ) (hA : 0 ≤ A) (avg : ℕ → (Fin d → ℤ) → BlockVec d) (h : ∀ (n : ℕ), (↑(triadicIndexBox d n).card)⁻¹ * ∑ w ∈ triadicIndexBox d n, blockVecDot (avg n w) (avg n w) ≤ A * 3 ^ (ρ * ↑n)) : Summable fun (n : ℕ) => 3 ^ ((↑t - ↑n) / 2) * √((↑(triadicIndexBox d n).card)⁻¹ * ∑ w ∈ triadicIndexBox d n, blockVecDot (avg n w) (avg n w))

The series defining the scale-average seminorm of AK.HC (2.130) is summable when the squared per-scale averages grow at most like A * 3 ^ (ρ * n) with ρ < 1, since each summand is then dominated by a geometric multiple of 3 ^ ((ρ - 1) / 2) < 1.

theorem HCPolySupport.HighContrast.Multiscale.besovSeminorm_le_of_scale_bound {d : ℕ} (t : ℤ) (ρ A : ℝ) (hρ : ρ < 1) (hρ0 : 0 ≤ ρ) (hA : 0 ≤ A) (avg : ℕ → (Fin d → ℤ) → BlockVec d) (h : ∀ (n : ℕ), (↑(triadicIndexBox d n).card)⁻¹ * ∑ w ∈ triadicIndexBox d n, blockVecDot (avg n w) (avg n w) ≤ A * 3 ^ (ρ * ↑n)) : besovSeminorm t avg ≤ 3 ^ (↑t / 2) * √A * (1 - 3 ^ ((ρ - 1) / 2))⁻¹

The scale-average seminorm of AK.HC (2.130) is bounded by the geometric series of its per-scale majorant: for a squared per-scale average at most A * 3 ^ (ρ * n) with ρ < 1, besovSeminorm t avg ≤ 3 ^ (t / 2) * sqrt A * (1 - 3 ^ ((ρ - 1) / 2))⁻¹.

theorem HCPolySupport.HighContrast.Multiscale.besovSeminorm_sq_le_of_scale_bound {d : ℕ} (t : ℤ) (ρ A : ℝ) (hρ : ρ < 1) (hρ0 : 0 ≤ ρ) (hA : 0 ≤ A) (avg : ℕ → (Fin d → ℤ) → BlockVec d) (h : ∀ (n : ℕ), (↑(triadicIndexBox d n).card)⁻¹ * ∑ w ∈ triadicIndexBox d n, blockVecDot (avg n w) (avg n w) ≤ A * 3 ^ (ρ * ↑n)) : besovSeminorm t avg ^ 2 ≤ (1 - 3 ^ ((ρ - 1) / 2))⁻¹ ^ 2 * (3 ^ ↑t * A)

Squared form of the preceding bound. For a squared per-scale average at most A * 3 ^ (ρ * n) with ρ < 1, besovSeminorm t avg ^ 2 ≤ ((1 - 3 ^ ((ρ - 1) / 2))⁻¹) ^ 2 * (3 ^ t * A).

Exact partition averaging for a cell average

The 3 ^ (n * d) depth-n triadic subcells adaptedCellAtCenter q (t - n) w, indexed by w ∈ triadicIndexBox d n, partition the adapted cell HighContrast.adaptedCell q t up to a null set, and all have the same volume. Hence the normalized sum of their averages of an integrable function is the average over the parent cell. This isolates the partition step used in the proof of the response weak estimate e.response.weak.estimate.

theorem HCPolySupport.HighContrast.Multiscale.triadicIndexBox_eq_centerSet {d : ℕ} (t : ℤ) (n : ℕ) : ↑(triadicIndexBox d n) = {w : Fin d → ℤ | standardCellCenter (t - ↑n) w ∈ centeredCube d t}

The triadic index box triadicIndexBox d n is exactly the set of depth-n index labels whose standard-cell center lies in the generation-t centered cube.

theorem HCPolySupport.HighContrast.Multiscale.avsum_volumeAverage_eq {d : ℕ} [NeZero d] (q : Mat d) (hq : IsUnit q) (t : ℤ) (n : ℕ) {f : Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f (adaptedCell q t) MeasureTheory.volume) : (↑(triadicIndexBox d n).card)⁻¹ * ∑ w ∈ triadicIndexBox d n, volumeAverage (adaptedCellAtCenter q (t - ↑n) w) f = volumeAverage (adaptedCell q t) f

Exact partition averaging: the normalized sum of the averages of an integrable function over the 3 ^ (n * d) depth-n triadic subcells equals the average over the adapted parent cell. This is the partition step in the proof of the response weak estimate e.response.weak.estimate.

The cell-average energy bound

The cell-average half of AK.HC (2.15): the doubled cell average of a b-harmonic field on a cell V is controlled by the pathwise symmetric energy of the field, with the constant supplied by the quadratic form of the coarse block of b on V augmented by the swap block 𝐑. The proof combines the variational (Fenchel) inequality satisfied by every admissible field with the canonical response--coarse-block identity on a bounded open convex domain.

theorem HCPolySupport.HighContrast.Multiscale.blockVecDot_self_le_of_forall_dot_le {d : ℕ} (W : BlockVec d) (B : BlockMat d) (E K : ℝ) (hK : 0 < K) (hB : ∀ (X : BlockVec d), blockVecDot X (blockMatVecMul B X) ≤ K * blockVecDot X X) (hvar : ∀ (X : BlockVec d), blockVecDot X W ≤ 1 / 2 * blockVecDot X (blockMatVecMul B X) + 1 / 2 * E) : blockVecDot W W ≤ K * E

Fenchel's algebraic core of the cell-average energy bound. A vector W that satisfies the variational inequality for the quadratic form of B is controlled by E as soon as B is bounded above by K times the identity form. This is the algebraic step of the cell-average half of AK.HC (2.15).

theorem HCPolySupport.HighContrast.Multiscale.forall_blockVecDot_cellAverage_optimizerField_le {d : ℕ} [NeZero d] {V : Set (Vec d)} {lam Lam : ℝ} {b : CoeffField d} (hConv : IsOpenBoundedConvexDomain V) (hEll : IsEllipticFieldOn lam Lam V b) (hvol : 0 < (MeasureTheory.volume V).toReal) (v : AHarmonicFunction b V) (X : BlockVec d) : blockVecDot X (blockMatVecMul (blockSwap d) (cellAverage V (optimizerField b v))) ≤ 1 / 2 * blockVecDot X (blockMatVecMul (ofFullBlockMat (toFullBlockMat (coarseBlockMatrix V b) + toFullBlockMat (blockSwap d))) X) + 1 / 2 * volumeAverage V (scalarVariationEnergyIntegrand b v)

The variational (Fenchel) inequality for the doubled cell average of a b-harmonic field on a cell V: for every doubled probe X, the pairing of X with the slot-swapped cell average of the optimizer field is bounded by half the quadratic form of the coarse block of b augmented by the swap block 𝐑, plus half the pathwise symmetric energy of the field. This is the variational step of the cell-average half of AK.HC (2.15), stated with the hypotheses of the canonical response--coarse-block identity on a bounded open convex domain.

theorem HCPolySupport.HighContrast.Multiscale.blockVecDot_cellAverage_optimizerField_self_le {d : ℕ} [NeZero d] {V : Set (Vec d)} {lam Lam : ℝ} {b : CoeffField d} (hConv : IsOpenBoundedConvexDomain V) (hEll : IsEllipticFieldOn lam Lam V b) (hvol : 0 < (MeasureTheory.volume V).toReal) (v : AHarmonicFunction b V) (K : ℝ) (hK : 0 < K) (hB : ∀ (X : BlockVec d), blockVecDot X (blockMatVecMul (ofFullBlockMat (toFullBlockMat (coarseBlockMatrix V b) + toFullBlockMat (blockSwap d))) X) ≤ K * blockVecDot X X) : blockVecDot (cellAverage V (optimizerField b v)) (cellAverage V (optimizerField b v)) ≤ K * volumeAverage V (scalarVariationEnergyIntegrand b v)

The cell-average energy bound: the squared doubled cell average of a b-harmonic field on a cell V is bounded by the pathwise symmetric energy of the field times any positive constant K that bounds above the quadratic form of the coarse block of b on V augmented by the swap block 𝐑. This is the cell-average half of AK.HC (2.15).