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

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

The scale-average seminorm and its positive-definiteness inputs

This file introduces the scale-average (Besov-type) seminorm besovSeminorm t avg used in the diagonal weak-norm bound of AK.HC (2.130), together with its cell-average family, its summability over scales, and the monotonicity of the associated ratio. It then supplies the positive- definiteness facts the diagonal weak-norm (cell-average) estimate needs: the annealed adapted mean and the block response mean are positive definite whenever the underlying coefficient sample is integrable, and the recentred energies respEhatMinus/respEhatPlus are positive definite from integrability or from a mean hypothesis, using that the response shear is a unit of the full block matrix. The scale-average seminorm and these positive-definiteness facts are the inputs to the response transfer of p.response.transfer.

HC bridge II: the scale-average seminorm (AK.HC (2.130))

The carrier is besovSeminorm t avg (ResponseBlockObjects.lean, real tsum); the ℝ≥0∞-valued adaptedWeakSeminorm q t s F is the alternative. The real carrier needs the summability supplied below. Paper p.response.transfer.

The pullback to the reference cube is in ReferenceCubeAveragePullback.lean; the diagonal weak-norm primal bound is in DiagonalDefectCarriers.lean / DiagonalWeakNormBound.lean.

noncomputable def HCPolySupport.HighContrast.Multiscale.cellAverageFamily {d : ℕ} (q : Mat d) (t : ℤ) (X : Vec d → BlockVec d) : ℕ → (Fin d → ℤ) → BlockVec d

The cell-average family of a doubled field on the selected grid: depth n, label w (old blockCellAverage ∘ adaptedCellAtCenter, WeakNorm.lean).

Equations

• HCPolySupport.HighContrast.Multiscale.cellAverageFamily q t X n w = HCPolySupport.HighContrast.Multiscale.cellAverage (HCPolySupport.HighContrast.adaptedCellAtCenter q (t - ↑n) w) X

noncomputable def HCPolySupport.HighContrast.Multiscale.cellMeanSq {d : ℕ} (V : Set (Vec d)) (X : Vec d → BlockVec d) : ℝ

The squared L²(U_t) mean of a doubled field.

Equations

• HCPolySupport.HighContrast.Multiscale.cellMeanSq V X = HCPolySupport.volumeAverage V fun (x : HCPolySupport.Vec d) => HCPolySupport.blockVecDot (X x) (X x)

Summability and the Jensen/partition bound

(p.response.transfer: a constant c has 3^{-t/2}[c] = |c|/(1-3^{-1/2}); the general field is bounded the same way through Jensen on each cell and exact partition averaging, p.response.transfer). Old counterpart: the ℝ≥0∞ sum needed no summability (WeakNorm.lean); the real carrier does.

HELPERS

theorem HCPolySupport.HighContrast.Multiscale.volumeAverage_mul_self_le {d : ℕ} {V : Set (Vec d)} (hV : MeasurableSet V) (hfin : MeasureTheory.volume V ≠ ⊤) (hvol : (MeasureTheory.volume V).toReal ≠ 0) {g : Vec d → ℝ} (hg : MeasureTheory.IntegrableOn g V MeasureTheory.volume) (hg2 : MeasureTheory.IntegrableOn (fun (x : Vec d) => g x * g x) V MeasureTheory.volume) : volumeAverage V g * volumeAverage V g ≤ volumeAverage V fun (x : Vec d) => g x * g x

Scalar Jensen for volumeAverage.

theorem HCPolySupport.HighContrast.Multiscale.sum_volumeAverage_mul_self_le {d : ℕ} {ι : Type u_1} [Fintype ι] {V : Set (Vec d)} (hV : MeasurableSet V) (hfin : MeasureTheory.volume V ≠ ⊤) (hvol : (MeasureTheory.volume V).toReal ≠ 0) (g : ι → Vec d → ℝ) (hG : MeasureTheory.IntegrableOn (fun (x : Vec d) => ∑ k : ι, g k x * g k x) V MeasureTheory.volume) : ∑ k : ι, volumeAverage V (g k) * volumeAverage V (g k) ≤ volumeAverage V fun (x : Vec d) => ∑ k : ι, g k x * g k x

Finite-family Jensen, junk-safe: non-integrable components contribute 0 on the left.

theorem HCPolySupport.HighContrast.Multiscale.blockVecDot_cellAverage_self_le_cellMeanSq {d : ℕ} {V : Set (Vec d)} (hV : MeasurableSet V) (hfin : MeasureTheory.volume V ≠ ⊤) (hvol : (MeasureTheory.volume V).toReal ≠ 0) (X : Vec d → BlockVec d) (hX : MeasureTheory.IntegrableOn (fun (x : Vec d) => blockVecDot (X x) (X x)) V MeasureTheory.volume) : blockVecDot (cellAverage V X) (cellAverage V X) ≤ cellMeanSq V X

Jensen for the doubled cell average: |(X)_V|² ≤ (|X|²)_V.

GEOMETRY. standardCell_subset_centeredCube_of_mem_triadicIndexBox and

adaptedCellAtCenter_subset_adaptedCell are imported from HCPoly/Entry/Response/Core/ScalarMaximizerExistence.lean.

theorem HCPolySupport.HighContrast.Multiscale.card_triadicIndexBox {d : ℕ} (n : ℕ) : ↑(triadicIndexBox d n).card = (3 ^ n) ^ d

theorem HCPolySupport.HighContrast.Multiscale.isOpen_adaptedCell_of_isUnit {d : ℕ} {q : Mat d} (hq : IsUnit q) (j : ℤ) : IsOpen (adaptedCell q j)

theorem HCPolySupport.HighContrast.Multiscale.isOpen_adaptedCellAtCenter_of_isUnit {d : ℕ} {q : Mat d} (hq : IsUnit q) (j : ℤ) (w : Fin d → ℤ) : IsOpen (adaptedCellAtCenter q j w)

The scale-term average bound

theorem HCPolySupport.HighContrast.Multiscale.avsum_cellAverageFamily_sq_le {d : ℕ} (q : Mat d) (hq : IsUnit q) (t : ℤ) (X : Vec d → BlockVec d) (hX : MeasureTheory.MemLp (fun (x : Vec d) => blockVecDot (X x) (X x)) 1 (MeasureTheory.volume.restrict (adaptedCell q t))) (n : ℕ) : (↑(triadicIndexBox d n).card)⁻¹ * ∑ w ∈ triadicIndexBox d n, blockVecDot (cellAverageFamily q t X n w) (cellAverageFamily q t X n w) ≤ cellMeanSq (adaptedCell q t) X

Each scale term is bounded by the L²(U_t) mean: Jensen on cells + exact partition of U_t by the 3^{nd} depth-n cells.

The geometric majorant

theorem HCPolySupport.HighContrast.Multiscale.three_rpow_scale_split (t : ℤ) (n : ℕ) : 3 ^ ((↑t - ↑n) / 2) = 3 ^ (↑t / 2) * (3 ^ (-(1 / 2))) ^ n

theorem HCPolySupport.HighContrast.Multiscale.besovRatio_lt_one : 3 ^ (-(1 / 2)) < 1

theorem HCPolySupport.HighContrast.Multiscale.besovRatio_nonneg : 0 ≤ 3 ^ (-(1 / 2))

theorem HCPolySupport.HighContrast.Multiscale.besov_term_le {d : ℕ} (q : Mat d) (hq : IsUnit q) (t : ℤ) (X : Vec d → BlockVec d) (hX : MeasureTheory.MemLp (fun (x : Vec d) => blockVecDot (X x) (X x)) 1 (MeasureTheory.volume.restrict (adaptedCell q t))) (n : ℕ) : 3 ^ ((↑t - ↑n) / 2) * √((↑(triadicIndexBox d n).card)⁻¹ * ∑ w ∈ triadicIndexBox d n, blockVecDot (cellAverageFamily q t X n w) (cellAverageFamily q t X n w)) ≤ 3 ^ (↑t / 2) * √(cellMeanSq (adaptedCell q t) X) * (3 ^ (-(1 / 2))) ^ n

The geometric majorant of the scale terms (avsum_cellAverageFamily_sq_le + monotonicity of sqrt).

Summability of the scale-term series

theorem HCPolySupport.HighContrast.Multiscale.summable_besov_cellAverageFamily {d : ℕ} (q : Mat d) (hq : IsUnit q) (t : ℤ) (X : Vec d → BlockVec d) (hX : MeasureTheory.MemLp (fun (x : Vec d) => blockVecDot (X x) (X x)) 1 (MeasureTheory.volume.restrict (adaptedCell q t))) : Summable fun (n : ℕ) => 3 ^ ((↑t - ↑n) / 2) * √((↑(triadicIndexBox d n).card)⁻¹ * ∑ w ∈ triadicIndexBox d n, blockVecDot (cellAverageFamily q t X n w) (cellAverageFamily q t X n w))

The series defining besovSeminorm is summable for an L²(U_t) field.

Positive definiteness of the annealed adapted mean from integrability alone

Every step of the cell-average estimate that consumes the response sample needs (toFullBlockMat (respMean P jStar F t)).PosDef, and that reduces by definition to (toFullBlockMat (adaptedMean P (respGrid jStar F) t)).PosDef. The tree previously obtained this only from Annealed.adaptedMean_posDef, which carries the whole coarse-ellipticity bundle; but the pathwise positivity of the coarse block uses nothing beyond IsUnit q, and the only genuinely missing input is the law-integrability of the coarse block. The two theorems below isolate that input, in the shape of the determinant bound 1 ≤ (toFullBlockMat (adaptedMean P q j)).det.

IsProbabilityMeasure P is not positivity content: it is the hypothesis under which the tree proves blockPosDef_annealedBlock (its expectation argument ends in measure_univ = 1), and blockPosDef_coarseBlock_adapted hides no ellipticity hypothesis — the local uniform ellipticity is carried by CoeffSpace d itself, and the only extra ingredient is IsUnit q, which the statement's hypothesis records.

theorem HCPolySupport.HighContrast.Multiscale.adaptedMean_posDef_of_integrable {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : IsUnit q) (j : ℤ) (hint : HasIntegrableCoarseBlock P (adaptedCell q j)) : Matrix.PosDef (toFullBlockMat (adaptedMean P q j))

The adapted annealed mean is positive definite as soon as its coarse block is law-integrable: IsUnit q supplies the pathwise positivity, and the expectation of an integrable family of positive blocks is positive.

theorem HCPolySupport.HighContrast.Multiscale.respMean_posDef_of_integrable {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {jStar : ℕ} {F : BlockMat d} (hgrid : IsUnit (respGrid jStar F)) (t : ℤ) (hint : HasIntegrableCoarseBlock P (respCell jStar F t)) : Matrix.PosDef (toFullBlockMat (respMean P jStar F t))

The response mean inherits the same positive definiteness, since respMean and respCell are adaptedMean and HighContrast.adaptedCell at the selected grid.

theorem HCPolySupport.HighContrast.Multiscale.isUnit_toFullBlockMat_respG {d : ℕ} (F : BlockMat d) : IsUnit (toFullBlockMat (respG F))

The response shear G = ⟨1, 0, respg F, 1⟩ is a unit for every F, with no hypothesis: the shear by -respg F is a right inverse, so the determinant is a unit.

theorem HCPolySupport.HighContrast.Multiscale.blockCongr_posDef {d : ℕ} {G E : BlockMat d} (hG : IsUnit (toFullBlockMat G)) (hE : Matrix.PosDef (toFullBlockMat E)) : Matrix.PosDef (toFullBlockMat (blockCongr G E))

Congruence by a unit preserves positive definiteness: conjugating a positive definite matrix by an invertible matrix keeps it positive definite (p.response.transfer).

theorem HCPolySupport.HighContrast.Multiscale.respEhatMinus_posDef_of_mean {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {jStar : ℕ} {F : BlockMat d} {t : ℤ} (hE : Matrix.PosDef (toFullBlockMat (respMean P jStar F t))) : Matrix.PosDef (toFullBlockMat (respEhatMinus P jStar F t))

The negative response sample Ehat^- = Gᵗ E_t G is positive definite as soon as the mean E_t is, since the shear G is a unit (p.response.transfer).

theorem HCPolySupport.HighContrast.Multiscale.respEhatPlus_posDef_of_mean {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {jStar : ℕ} {F : BlockMat d} {t : ℤ} (hE : Matrix.PosDef (toFullBlockMat (respMean P jStar F t))) : Matrix.PosDef (toFullBlockMat (respEhatPlus P jStar F t))

The positive response sample Ehat^+ = D Ehat^- D is positive definite as soon as the mean is, since the doubling D is a unit (p.response.transfer).

theorem HCPolySupport.HighContrast.Multiscale.respEhatMinus_posDef_of_integrable {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {jStar : ℕ} {F : BlockMat d} (hgrid : IsUnit (respGrid jStar F)) (t : ℤ) (hint : HasIntegrableCoarseBlock P (respCell jStar F t)) : Matrix.PosDef (toFullBlockMat (respEhatMinus P jStar F t))

The response sample is positive definite as soon as the coarse block is law-integrable. Composing the congruence step with respMean_posDef_of_integrable, the positive definiteness that the recent-head chain asks of Ê⁻ rests on exactly two things a caller can hold: the unit selected grid that the cell-average estimate already carries, and the integrability of the coarse block under the law. Neither stationarity, nor the coarse-ellipticity bundle, nor a dimension bound is used.

theorem HCPolySupport.HighContrast.Multiscale.respEhatPlus_posDef_of_integrable {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {jStar : ℕ} {F : BlockMat d} (hgrid : IsUnit (respGrid jStar F)) (t : ℤ) (hint : HasIntegrableCoarseBlock P (respCell jStar F t)) : Matrix.PosDef (toFullBlockMat (respEhatPlus P jStar F t))

The adjoint twin of respEhatMinus_posDef_of_integrable.