High-contrast homogenization: Provider.PortableHistory.MajorizationSup

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

The centered maximum as a statistic

Three facts about the supremum in e.scale.selection.fluctuation.history are used by the majorization argument of p.fixed.geometry.one.grid.propagation, and none of them depends on which range of scales or which family of cells the supremum runs over.

Maximum to sum. The Q-th power of a maximum over a finite family is at most the sum of the Q-th powers. This is the step the printed proof calls "max-to-sum", and it is what converts a maximum over the 3^{d(T-b)} children of the terminal cell into a sum with the counting factor in front.

Measurability. The supremum runs over countably many scales and countably many aligned centers, and each term is a continuous function of the entries of the coarse response; the measurability of the variational coarse block therefore makes the whole maximum a measurable statistic, which is what allows the sum to be integrated term by term.

Change of variables. Under stationarity of the coefficient law an integer translation preserves the law, so the lower integral of any statistic is unchanged when the sample is translated.

The last statement recorded here is the centered moment v_j^q of p.fixed.geometry.one.grid.propagation written as the lower integral of the Q-th power of the Schatten size, which is the form in which the scales above the checkpoint are summed.

Maximum to sum

theorem HCPolySupport.HighContrast.PortableHistory.iSup_finset_rpow_le_sum {ι : Type u_1} (s : Finset ι) (f : ι → ENNReal) {Q : ℝ} (hQ : 0 < Q) : (⨆ i ∈ s, f i) ^ Q ≤ ∑ i ∈ s, f i ^ Q

Max-to-sum. The Q-th power of a maximum over a finite family is at most the sum of the Q-th powers.

theorem HCPolySupport.HighContrast.PortableHistory.three_rpow_admissible_le {Q a rhoMax dd u lam g : ℝ} (hadm : a ≤ Q * rhoMax - dd) (hu : 0 ≤ u) (hlam : 0 ≤ lam) (hlamg : lam ^ Q ≤ g) : (3 ^ (-rhoMax * u) * lam) ^ Q * 3 ^ (dd * u) ≤ 3 ^ (-a * u) * g

The admissibility a ≤ Qρ_max - d absorbs the counting factor. The weight of a scale gap u, raised to the power Q and multiplied by the number 3^{du} of cells of that gap, is at most the weight 3^{-au} times whatever dominates the Q-th power of the renormalization cost.

The centered maximum is measurable

theorem HCPolySupport.HighContrast.PortableHistory.aemeasurable_adaptedSup {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) {F : BlockMat d} (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) (g : ℤ → ℝ) (jlo jhi : ℤ) (S : Set (Vec d)) : AEMeasurable (fun (x : CoeffSpace d) => ⨆ (j : ℤ), ⨆ (_ : jlo ≤ j), ⨆ (_ : j ≤ jhi), ⨆ (w : Fin d → ℤ), ⨆ (_ : adaptedCellCenter q j w ∈ S), ENNReal.ofReal (g j * blockSize (blockSub (adaptedResponse q j w x) (adaptedMean P q j)) F)) P

The centered maximum is a measurable statistic. Countably many scales, countably many aligned centers, and a scalar size that is a continuous function of the entries of the response.

theorem HCPolySupport.HighContrast.PortableHistory.aemeasurable_adaptedCellSup {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) {F : BlockMat d} (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) (c : ℝ) (j : ℤ) (S : Set (Vec d)) : AEMeasurable (fun (x : CoeffSpace d) => ⨆ (w : Fin d → ℤ), ⨆ (_ : adaptedCellCenter q j w ∈ S), ENNReal.ofReal (c * blockSize (blockSub (adaptedResponse q j w x) (adaptedMean P q j)) F)) P

The centered maximum over the aligned cells of one scale is a measurable statistic.

Change of variables along an integer translation

theorem HCPolySupport.HighContrast.PortableHistory.lintegral_comp_translateCoeff {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hP : IsStationaryLaw P) {f : CoeffSpace d → ENNReal} (hf : AEMeasurable f P) (z : Fin d → ℤ) : ∫⁻ (x : CoeffSpace d), f (translateCoeff z x) ∂P = ∫⁻ (x : CoeffSpace d), f x ∂P

An integer translation does not move a lower integral. This is stationarity of the coefficient law read through the change of variables.

theorem HCPolySupport.HighContrast.PortableHistory.lintegral_iSup_translate_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hP : IsStationaryLaw P) {Q : ℝ} (hQ : 0 < Q) {F : CoeffSpace d → ENNReal} (hF : AEMeasurable F P) (Z : Finset (Fin d → ℤ)) (v : (Fin d → ℤ) → Fin d → ℤ) : ∫⁻ (x : CoeffSpace d), (⨆ y ∈ Z, F (translateCoeff (v y) x)) ^ Q ∂P ≤ ↑Z.card * ∫⁻ (x : CoeffSpace d), F x ^ Q ∂P

Max-to-sum over the children of a cell. A maximum over a finite family of translates is integrated term by term, and every term contributes the same lower integral by stationarity of the coefficient law; only the cardinality survives.

The centered moment as a lower integral

theorem HCPolySupport.HighContrast.PortableHistory.centeredMoment_rpow {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {Q : ℝ} (hQ : 0 < Q) (q : Mat d) (j : ℤ) (hmeas : MeasureTheory.AEStronglyMeasurable (fun (x : CoeffSpace d) => schattenSize Q (blockSub (coarseBlock (adaptedCell q j) x) (adaptedMean P q j)) (adaptedMean P q j)) P) : centeredMoment P Q q j ^ Q = ∫⁻ (x : CoeffSpace d), ENNReal.ofReal (schattenSize Q (blockSub (coarseBlock (adaptedCell q j) x) (adaptedMean P q j)) (adaptedMean P q j)) ^ Q ∂P

The Q-th power of the centered moment v_j^q is the lower integral of the Q-th power of the Schatten size.