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

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

Pullback to the reference cube

For the linear change of variables x = q y, this file transports the Lebesgue measure, cube averages and the doubled-field integrability along the pullback, and identifies the depth-n descendant cells of the reference cube, indexed by the triadic index box, with the image of the corresponding translated origin cubes. It records the injectivity and measurability the transport needs, the volume of a translated cube, and the metric comparison between the rounded and unrounded grid bounding the pullback's operator norm. It also supplies, for the recentred coefficient families a_- and a_+, the existence of a scalar canonical response maximizer on every aligned subcell of the terminal generation. The module serves the manuscript's p.response.transfer.

HC bridge II (B5): pullback to the reference cube

Paper p.response.transfer. Depends on ScaleAverageSeminorm.lean (B4).

B5. Pullback to the reference cube: the eccentricity-free constant

(p.response.transfer). Old: adaptedWeakSeminorm_affinePullback_le (HCPoly/Provider/Response/AdaptedWeakTransport.lean), explicitRoundedGrid_metricFrobenius_product_le (AdaptedWeakProduct.lean), and the slotwise bridges ofReal_partialSeminorm_metricPullback_fst_le_separate/_snd_) to the CG seminorm cubeBesovNegativeVectorPartialSeminorm (Deterministic/WeakNormInterfaces/Definitions.lean).

HELPERS — all CLOSED, new declarations to be pasted alongside the theorems.

theorem HCPolySupport.HighContrast.Multiscale.opNorm_inv_pos {d : ℕ} [NeZero d] {m : Mat d} (hm : Matrix.PosDef m) : 0 < ‖m⁻¹‖

theorem HCPolySupport.HighContrast.Multiscale.inverseNormLE_unroundedGrid {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) : Geometry.InverseNormLE (Geometry.unroundedGrid m) 1

theorem HCPolySupport.HighContrast.Multiscale.isUnit_det_unroundedGrid {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) : IsUnit (Matrix.det (Geometry.unroundedGrid m))

theorem HCPolySupport.HighContrast.Multiscale.opNorm_unroundedGrid_inv_le {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) : ‖(Geometry.unroundedGrid m)⁻¹‖ ≤ 1

theorem HCPolySupport.HighContrast.Multiscale.norm_one_mat {d : ℕ} [NeZero d] : ‖1‖ = 1

theorem HCPolySupport.HighContrast.Multiscale.opNorm_metric_product_le {d : ℕ} [NeZero d] {l : ℕ} (hl : 2 * d ≤ 3 ^ l) {m : Mat d} (hm : Matrix.PosDef m) : ‖(Geometry.unroundedGrid m)⁻¹ * Geometry.explicitRoundedGrid l m‖ * ‖(Geometry.explicitRoundedGrid l m)⁻¹ * Geometry.unroundedGrid m‖ ≤ 3

theorem HCPolySupport.HighContrast.Multiscale.explicitRoundedGrid_metricFrobenius_product_le {d : ℕ} [NeZero d] (l : ℕ) (hl : 2 * d ≤ 3 ^ l) (m : Mat d) (hm : Matrix.PosDef m) : √(Book.Ch02.matrixFrobeniusNormSq (matTranspose (Geometry.explicitRoundedGrid l m) * (matSqrt m)⁻¹)) * √(Book.Ch02.matrixFrobeniusNormSq ((Geometry.explicitRoundedGrid l m)⁻¹ * matSqrt m)) ≤ 3 * ↑d ^ 2

|q^T m^{-1/2}|_F |q^{-1} m^{1/2}|_F ≤ 3 d² for q = explicitRoundedGrid l m (old AdaptedWeakProduct.lean; paper p.response.transfer, ≤ 3 in operator norm).

The old 51/50 · d² needed kZero d ≤ l; on the current carrier only the repo-standing 2 * d ≤ 3 ^ l (HCPoly/Entry/Geometry/RoundedGridBasic.lean) is available, which gives the paper's own constant 3 instead.

theorem HCPolySupport.HighContrast.Multiscale.continuous_matVecMul {d : ℕ} (q : Mat d) : Continuous (matVecMul q)

theorem HCPolySupport.HighContrast.Multiscale.measurable_matVecMul {d : ℕ} (q : Mat d) : Measurable (matVecMul q)

noncomputable def HCPolySupport.HighContrast.Multiscale.matMeasurableEquiv {d : ℕ} {q : Mat d} (hq : IsUnit q) : Vec d ≃ᵐ Vec d

The invertible linear map x ↦ q x as a measurable equivalence.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Multiscale.map_matVecMul_volume {d : ℕ} {q : Mat d} (hq : IsUnit q) : MeasureTheory.Measure.map (matVecMul q) MeasureTheory.volume = ENNReal.ofReal |Matrix.det q|⁻¹ • MeasureTheory.volume

theorem HCPolySupport.HighContrast.Multiscale.setIntegral_comp_matVecMul {d : ℕ} {q : Mat d} (hq : IsUnit q) {A : Set (Vec d)} (hA : MeasurableSet A) (g : Vec d → ℝ) : ∫ (y : Vec d) in matVecMul q ⁻¹' A, g (matVecMul q y) = |Matrix.det q|⁻¹ * ∫ (x : Vec d) in A, g x

Stage 2 : cube-average pullback

theorem HCPolySupport.HighContrast.Multiscale.injective_matVecMul {d : ℕ} {q : Mat d} (hq : IsUnit q) : Function.Injective (matVecMul q)

theorem HCPolySupport.HighContrast.Multiscale.preimage_matVecMul_adaptedCellAtCenter {d : ℕ} {q : Mat d} (hq : IsUnit q) (k : ℤ) (w : Fin d → ℤ) : matVecMul q ⁻¹' adaptedCellAtCenter q k w = openCubeSet (translateCube w (originCube d k))

theorem HCPolySupport.HighContrast.Multiscale.cubeVolume_translateCube_originCube {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : cubeVolume (translateCube w (originCube d k)) = (3 ^ k) ^ d

theorem HCPolySupport.HighContrast.Multiscale.volume_adaptedCellAtCenter_toReal {d : ℕ} (q : Mat d) (k : ℤ) (w : Fin d → ℤ) : (MeasureTheory.volume (adaptedCellAtCenter q k w)).toReal = |Matrix.det q| * (3 ^ k) ^ d

theorem HCPolySupport.HighContrast.Multiscale.cubeAverage_comp_matVecMul {d : ℕ} {q : Mat d} (hq : IsUnit q) (k : ℤ) (w : Fin d → ℤ) (g : Vec d → ℝ) : (cubeAverage (translateCube w (originCube d k)) fun (y : Vec d) => g (matVecMul q y)) = volumeAverage (adaptedCellAtCenter q k w) g

theorem HCPolySupport.HighContrast.Multiscale.cubeAverageVec_comp_matVecMul {d : ℕ} {q : Mat d} (hq : IsUnit q) (k : ℤ) (w : Fin d → ℤ) (Y : Vec d → Vec d) : (cubeAverageVec (translateCube w (originCube d k)) fun (y : Vec d) => Y (matVecMul q y)) = volumeAverageVec (adaptedCellAtCenter q k w) Y

theorem HCPolySupport.HighContrast.Multiscale.volumeAverageVec_matVecMul {d : ℕ} {A : Set (Vec d)} (W : Mat d) (Y : Vec d → Vec d) (hY : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => Y x i) A MeasureTheory.volume) : (volumeAverageVec A fun (x : Vec d) => matVecMul W (Y x)) = matVecMul W (volumeAverageVec A Y)

Stage 3 : index bridge

theorem HCPolySupport.HighContrast.Multiscale.mem_triadicIndexBox_iff {d n : ℕ} {w : Fin d → ℤ} : w ∈ triadicIndexBox d n ↔ ∀ (i : Fin d), |w i| ≤ ↑((3 ^ n - 1) / 2)

theorem HCPolySupport.HighContrast.Multiscale.triadicIndexBound_succ (n : ℕ) : ↑((3 ^ (n + 1) - 1) / 2) = 3 * ↑((3 ^ n - 1) / 2) + 1

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

theorem HCPolySupport.HighContrast.Multiscale.index_mem_triadicIndexBox_of_mem_descendantsAtDepth {d : ℕ} (t : ℤ) (n : ℕ) (R : TriadicCube d) : R ∈ descendantsAtDepth (originCube d t) n → R.index ∈ triadicIndexBox d n

theorem HCPolySupport.HighContrast.Multiscale.injective_translateCube_originCube {d : ℕ} (k : ℤ) : Function.Injective fun (w : Fin d → ℤ) => translateCube w (originCube d k)

theorem HCPolySupport.HighContrast.Multiscale.descendantsAtDepth_originCube_eq_image {d : ℕ} (t : ℤ) (n : ℕ) : descendantsAtDepth (originCube d t) n = Finset.image (fun (w : Fin d → ℤ) => translateCube w (originCube d (t - ↑n))) (triadicIndexBox d n)

theorem HCPolySupport.HighContrast.Multiscale.descendantsAverage_originCube_eq {d : ℕ} (t : ℤ) (n : ℕ) (F : TriadicCube d → ℝ) : descendantsAverage (originCube d t) n F = (↑(triadicIndexBox d n).card)⁻¹ * ∑ w ∈ triadicIndexBox d n, F (translateCube w (originCube d (t - ↑n)))

Stage 4 : core inequalities

theorem HCPolySupport.HighContrast.Multiscale.matVecMul_mul_apply {d : ℕ} (A B : Mat d) (v : Vec d) : matVecMul (A * B) v = matVecMul A (matVecMul B v)

theorem HCPolySupport.HighContrast.Multiscale.vecNormSq_fst_le_blockVecDot {d : ℕ} (Y : BlockVec d) : vecNormSq Y.1 ≤ blockVecDot Y Y

theorem HCPolySupport.HighContrast.Multiscale.vecNormSq_snd_le_blockVecDot {d : ℕ} (Y : BlockVec d) : vecNormSq Y.2 ≤ blockVecDot Y Y

theorem HCPolySupport.HighContrast.Multiscale.integrableOn_apply_of_vecNormSq_le {d : ℕ} {U : Set (Vec d)} (hUfin : MeasureTheory.volume U ≠ ⊤) {Y : Vec d → Vec d} (hYm : MeasureTheory.AEStronglyMeasurable Y (MeasureTheory.volume.restrict U)) {f : Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f U MeasureTheory.volume) (hle : ∀ (x : Vec d), vecNormSq (Y x) ≤ f x) (i : Fin d) : MeasureTheory.IntegrableOn (fun (x : Vec d) => Y x i) U MeasureTheory.volume

theorem HCPolySupport.HighContrast.Multiscale.depthAverage_pullback_le {d : ℕ} {q : Mat d} (hq : IsUnit q) (W : Mat d) (t : ℤ) (n : ℕ) (Z : Vec d → BlockVec d) (sl : BlockVec d → Vec d) (hsl_lin : ∀ (V : Set (Vec d)), (volumeAverageVec V fun (x : Vec d) => sl (Z x)) = sl (cellAverage V Z)) (hsl_le : ∀ (Y : BlockVec d), vecNormSq (sl Y) ≤ blockVecDot Y Y) (hint : ∀ w ∈ triadicIndexBox d n, ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => sl (Z x) i) (adaptedCellAtCenter q (t - ↑n) w) MeasureTheory.volume) : cubeBesovNegativeVectorDepthAverage (originCube d t) (fun (y : Vec d) => matVecMul W (sl (Z (matVecMul q y)))) n ≤ Book.Ch02.matrixFrobeniusNormSq W * ((↑(triadicIndexBox d n).card)⁻¹ * ∑ w ∈ triadicIndexBox d n, blockVecDot (cellAverage (adaptedCellAtCenter q (t - ↑n) w) Z) (cellAverage (adaptedCellAtCenter q (t - ↑n) w) Z))

theorem HCPolySupport.HighContrast.Multiscale.partialSeminorm_le_tsum_core {d : ℕ} (t : ℤ) (N : ℕ) (C : ℝ) (hC : 0 ≤ C) (u : Vec d → Vec d) (inner : ℕ → ℝ) (hdepth : ∀ (n : ℕ), cubeBesovNegativeVectorDepthAverage (originCube d t) u n ≤ C ^ 2 * inner n) (hsum : Summable fun (n : ℕ) => 3 ^ ((↑t - ↑n) / 2) * √(inner n)) : cubeBesovNegativeVectorPartialSeminorm (originCube d t) (1 / 2) N u ≤ 3 ^ (-(↑t / 2)) * C * ∑' (n : ℕ), 3 ^ ((↑t - ↑n) / 2) * √(inner n)

Stage 5 : the slotwise pullback bound and the two theorems

theorem HCPolySupport.HighContrast.Multiscale.partialSeminorm_pullback_slot_le {d : ℕ} {q : Mat d} (hq : IsUnit q) (W : Mat d) (t : ℤ) (N : ℕ) (Z : Vec d → BlockVec d) (sl : BlockVec d → Vec d) (hsl_lin : ∀ (V : Set (Vec d)), (volumeAverageVec V fun (x : Vec d) => sl (Z x)) = sl (cellAverage V Z)) (hsl_le : ∀ (Y : BlockVec d), vecNormSq (sl Y) ≤ blockVecDot Y Y) (hZm : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => sl (Z x)) (MeasureTheory.volume.restrict (adaptedCell q t))) (hX : MeasureTheory.MemLp (fun (x : Vec d) => blockVecDot (Z x) (Z x)) 1 (MeasureTheory.volume.restrict (adaptedCell q t))) : (cubeBesovNegativeVectorPartialSeminorm (originCube d t) (1 / 2) N fun (y : Vec d) => matVecMul W (sl (Z (matVecMul q y)))) ≤ 3 ^ (-(↑t / 2)) * √(Book.Ch02.matrixFrobeniusNormSq W) * besovSeminorm t (cellAverageFamily q t Z)

theorem HCPolySupport.HighContrast.Multiscale.partialSeminorm_pullback_fst_le {d : ℕ} [NeZero d] (q : Mat d) (hq : IsUnit q) (m : Mat d) (hm : Matrix.PosDef m) (t : ℤ) (N : ℕ) (X : Vec d → BlockVec d) (hX : MeasureTheory.MemLp (fun (x : Vec d) => blockVecDot (matVecMul (matSqrt m) (X x).1, matVecMul (matSqrt m)⁻¹ (X x).2) (matVecMul (matSqrt m) (X x).1, matVecMul (matSqrt m)⁻¹ (X x).2)) 1 (MeasureTheory.volume.restrict (adaptedCell q t))) (hXm : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => (matVecMul (matSqrt m) (X x).1, matVecMul (matSqrt m)⁻¹ (X x).2)) (MeasureTheory.volume.restrict (adaptedCell q t))) : (cubeBesovNegativeVectorPartialSeminorm (originCube d t) (1 / 2) N fun (y : Vec d) => matVecMul (matTranspose q) (X (matVecMul q y)).1) ≤ 3 ^ (-(↑t / 2)) * √(Book.Ch02.matrixFrobeniusNormSq (matTranspose q * (matSqrt m)⁻¹)) * besovSeminorm t (cellAverageFamily q t fun (x : Vec d) => (matVecMul (matSqrt m) (X x).1, matVecMul (matSqrt m)⁻¹ (X x).2))

The pullback bound for the first slot: the negative Besov seminorm up to depth N of y ↦ matVecMul (matTranspose q) (X (matVecMul q y)).1 is at most 3 ^ (-t/2) times the Frobenius factor Real.sqrt (matrixFrobeniusNormSq (matTranspose q * (matSqrt m)⁻¹)) times the Besov seminorm of the cell-average family of the block field.

theorem HCPolySupport.HighContrast.Multiscale.partialSeminorm_pullback_snd_le {d : ℕ} [NeZero d] (q : Mat d) (hq : IsUnit q) (m : Mat d) (hm : Matrix.PosDef m) (t : ℤ) (N : ℕ) (X : Vec d → BlockVec d) (hX : MeasureTheory.MemLp (fun (x : Vec d) => blockVecDot (matVecMul (matSqrt m) (X x).1, matVecMul (matSqrt m)⁻¹ (X x).2) (matVecMul (matSqrt m) (X x).1, matVecMul (matSqrt m)⁻¹ (X x).2)) 1 (MeasureTheory.volume.restrict (adaptedCell q t))) (hXm : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => (matVecMul (matSqrt m) (X x).1, matVecMul (matSqrt m)⁻¹ (X x).2)) (MeasureTheory.volume.restrict (adaptedCell q t))) : (cubeBesovNegativeVectorPartialSeminorm (originCube d t) (1 / 2) N fun (y : Vec d) => matVecMul q⁻¹ (X (matVecMul q y)).2) ≤ 3 ^ (-(↑t / 2)) * √(Book.Ch02.matrixFrobeniusNormSq (q⁻¹ * matSqrt m)) * besovSeminorm t (cellAverageFamily q t fun (x : Vec d) => (matVecMul (matSqrt m) (X x).1, matVecMul (matSqrt m)⁻¹ (X x).2))

The pullback bound for the second slot: the negative Besov seminorm up to depth N of y ↦ matVecMul q⁻¹ (X (matVecMul q y)).2 is at most 3 ^ (-t/2) times the Frobenius factor Real.sqrt (matrixFrobeniusNormSq (q⁻¹ * matSqrt m)) times the Besov seminorm of the cell-average family of the block field.

Response maximizers on every aligned subcell

The terminal-optimizer replacement of p.response.transfer compares the optimizer of the terminal cell with the optimizer of each aligned subcell z + ⋄_j^q of the coarse scale. This module supplies the existence input for that comparison: for the recentred coefficient families a_- and a_+ and for every sample, a scalar canonical response maximizer exists on each translated aligned cell adaptedCellAtCenter q j w. The centered-cell statements nonempty_scalarCanonicalMaximizer_respCoeffMinus and ..._respCoeffPlus are transported to the translate by exhibiting the translate as an affine image of the centered adapted cell, which is open, bounded, convex and nonempty.

theorem HCPolySupport.HighContrast.Multiscale.nonempty_scalarCanonicalMaximizer_respCoeffMinus_adaptedCellAtCenter {d : ℕ} (q : Mat d) (hq : IsUnit q) (j : ℤ) (w : Fin d → ℤ) (F : BlockMat d) (a : CoeffSpace d) (p r : Vec d) : Nonempty (ScalarCanonicalMaximizer (adaptedCellAtCenter q j w) p r (respCoeffMinus F a))

Existence of a scalar canonical maximizer for a_- = a - g on the translated aligned cell z + ⋄_j^q at z = 3^j q w, the aligned subcell produced by subdividing the coarse scale. This is the translate of nonempty_scalarCanonicalMaximizer_respCoeffMinus to the recentred coefficient a_-.

theorem HCPolySupport.HighContrast.Multiscale.nonempty_scalarCanonicalMaximizer_respCoeffPlus_adaptedCellAtCenter {d : ℕ} (q : Mat d) (hq : IsUnit q) (j : ℤ) (w : Fin d → ℤ) (F : BlockMat d) (a : CoeffSpace d) (p r : Vec d) : Nonempty (ScalarCanonicalMaximizer (adaptedCellAtCenter q j w) p r (respCoeffPlus F a))

Existence of a scalar canonical maximizer for a_+ = a^t + g on the translated aligned cell z + ⋄_j^q at z = 3^j q w, the aligned subcell produced by subdividing the coarse scale. This is the translate of nonempty_scalarCanonicalMaximizer_respCoeffPlus to the recentred coefficient a_+.