High-contrast homogenization: Setup.SourceObjects

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

Source-window and source-control carriers

The objects of the source-control subsection and of the random-source window: the geometric series ζ_g, χ_g, the witness eccentricity 𝔢_q and the boundary constant B_q, the cross-grid factor K(q,q'), the dual reference block 𝐄_* and the reference ratio κ_𝐄, the source growth witness K_bar_S, the weak-Orlicz moment multiplier 𝔐_p, the source burn j_S, the coupled window pair, the source-remainder scale a_{j_*}^S, the fixed-history exponents, and the window multiplier Y_P presented as data together with the properties the window lemma establishes for it.

Λ(F;𝐄) = |F^{-1/2}𝐄F^{-1/2}| is blockSize 𝐄 F, and |𝐄^{-1/2}𝐀(V)𝐄^{-1/2}| is blockSize (coarseBlock V a) 𝐄; the single carrier blockSize serves both, and the sharp-adjoint normalization |𝐄_*^{1/2}𝐀_*^{-1}(V)𝐄_*^{1/2}| is blockSize (coarseStarInv V a) (blockReflect 𝐄), the dual reference block being 𝐄_*^{-1} = R 𝐄 R.

The sharp-adjoint response

noncomputable def HCPolySupport.HighContrast.coarseStarInv {d : ℕ} (U : Set (Vec d)) (a : CoeffSpace d) : BlockMat d

The inverse sharp-adjoint coarse response 𝐀_*^{-1}(U; a) (the dual of the coarse block).

Equations

• HCPolySupport.HighContrast.coarseStarInv U a = HCPolySupport.coarseStarredBlockMatrixInv U ↑↑a

The geometric series and the grid constants

noncomputable def HCPolySupport.HighContrast.zetaG (g : ℝ) : ℝ

ζ_g = Σ_{u ≥ 0} 3^{-(1-g)u} = (1 - 3^{-(1-g)})^{-1}, for 0 ≤ g < 1.

Equations

• HCPolySupport.HighContrast.zetaG g = (1 - 3 ^ (-(1 - g)))⁻¹

noncomputable def HCPolySupport.HighContrast.chiG (g : ℝ) : ℝ

χ_g = Σ_{u ≥ 1} 3^{-(1-g)u} = (3^{1-g} - 1)^{-1}, for 0 ≤ g < 1.

Equations

• HCPolySupport.HighContrast.chiG g = (3 ^ (1 - g) - 1)⁻¹

noncomputable def HCPolySupport.HighContrast.witnessEccentricity {d : ℕ} (m : Mat d) : ℝ

The witness eccentricity 𝔢_q = (|m| |m^{-1}|)^{1/2} of a rounded grid presented with its positive witness m; a function of the witness alone.

Equations

• HCPolySupport.HighContrast.witnessEccentricity m = √(HCPolySupport.HighContrast.specBound m * HCPolySupport.HighContrast.specBound m⁻¹)

noncomputable def HCPolySupport.HighContrast.boundaryConst {d : ℕ} (Cd g : ℝ) (m : Mat d) : ℝ

The boundary constant B_q = C_d 𝔢_q ζ_g, with the dimensional constant of the source-control subsection carried explicitly.

Equations

• HCPolySupport.HighContrast.boundaryConst Cd g m = Cd * HCPolySupport.HighContrast.witnessEccentricity m * HCPolySupport.HighContrast.zetaG g

noncomputable def HCPolySupport.HighContrast.gridRatio {d : ℕ} (q q' : Mat d) : ℝ

The cross-grid factor K(q,q') = (1 + |q^{-1}q'| + |(q')^{-1}q|)^{2d}.

Equations

• HCPolySupport.HighContrast.gridRatio q q' = (1 + ‖q⁻¹ * q'‖ + ‖q'⁻¹ * q‖) ^ (2 * d)

noncomputable def HCPolySupport.HighContrast.kappaRef {d : ℕ} (E : BlockMat d) : ℝ

The reference ratio κ_𝐄 = |𝐄_*^{-1/2}𝐄𝐄_*^{-1/2}|.

Equations

• HCPolySupport.HighContrast.kappaRef E = HCPolySupport.HighContrast.blockSize E (HCPolySupport.HighContrast.blockSharp E)

The source gauge, the burn, and the window

def HCPolySupport.HighContrast.growthBar (K : ℝ) : ℝ

K_bar_S = max{2, K_{Ψ_S}}.

Equations

• HCPolySupport.HighContrast.growthBar K = max 2 K

noncomputable def HCPolySupport.HighContrast.momentMultiplier (p Kbar : ℝ) : ℝ

The weak-Orlicz moment multiplier 𝔐_p(K_bar) = (1 + 2p K_bar^{⌈p(p+1)/2⌉}(1 + log K_bar))^{1/p} (the moment bound for the source scale furnished by its tail gauge).

Equations

• HCPolySupport.HighContrast.momentMultiplier p Kbar = (1 + 2 * p * Kbar ^ ⌈p * (p + 1) / 2⌉ * (1 + Real.log Kbar)) ^ p⁻¹

noncomputable def HCPolySupport.HighContrast.sourceBurn (d : ℕ) (Q K : ℝ) : ℤ

The source burn j_S (e.source.lower.scale).

Equations

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

def HCPolySupport.HighContrast.IsCoupledWindow (d : ℕ) (Q K : ℝ) (jStar M : ℤ) : Prop

A coupled window pair (j_*, M) (the containing window on which the single source multiplier is built).

Equations

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

noncomputable def HCPolySupport.HighContrast.sourceRemainderScale (d : ℕ) (jStar : ℤ) (K : ℝ) : ℝ

The source-remainder scale a_{j_*}^S = K_bar_S^{4(d+1)}3^{2-j_*} (the residual source parameter at the lower generation).

Equations

• HCPolySupport.HighContrast.sourceRemainderScale d jStar K = HCPolySupport.HighContrast.growthBar K ^ (4 * (d + 1)) * 3 ^ (2 - jStar)

noncomputable def HCPolySupport.HighContrast.burnDiscount (g : ℝ) (jStar a : ℤ) : ℝ

The positive-part discount 3^{g(j_* - a)_+} carried by every cell bound of the window (e.source.adapted.bound).

Equations

• HCPolySupport.HighContrast.burnDiscount g jStar a = 3 ^ (g * max (↑jStar - ↑a) 0)

The fixed-history exponents

noncomputable def HCPolySupport.HighContrast.initExpQ (d : ℕ) (g : ℝ) : ℕ

Q = 2⌈2(d+1)/(1-g)⌉ (e.scale.selection.Q.choice).

Equations

• HCPolySupport.HighContrast.initExpQ d g = 2 * ⌈2 * (↑d + 1) / (1 - g)⌉₊

noncomputable def HCPolySupport.HighContrast.initExpA (g : ℝ) : ℝ

a = (1-g)/4 (e.scale.selection.Q.choice).

Equations

• HCPolySupport.HighContrast.initExpA g = (1 - g) / 4

noncomputable def HCPolySupport.HighContrast.initExpRhoMax (d : ℕ) (g : ℝ) : ℝ

ρ_max = g + (d + a)/Q (e.scale.selection.Q.choice).

Equations

• HCPolySupport.HighContrast.initExpRhoMax d g = g + (↑d + HCPolySupport.HighContrast.initExpA g) / ↑(HCPolySupport.HighContrast.initExpQ d g)

noncomputable def HCPolySupport.HighContrast.initExpRhoDr (g : ℝ) : ℝ

ρ_dr = a/2 (e.scale.selection.Q.choice).

Equations

• HCPolySupport.HighContrast.initExpRhoDr g = HCPolySupport.HighContrast.initExpA g / 2

The window multiplier as data

structure HCPolySupport.HighContrast.IsWindowMultiplier {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (g : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K Cd : ℝ) (jStar M : ℤ) (Y : CoeffSpace d → ℝ) : Prop

The common source multiplier of a bounded window, presented as data with exactly the properties e.source.multiplier establishes for it: it is at least one, it dominates the coarse response and its sharp adjoint on every standard aligned cube and on every adapted cell of every deterministic rounded grid at alignment j_* inside the window, simultaneously and on one event of full measure, and its excess over one has the source gauge's weak-Orlicz tail at the remainder scale, with the resulting L^p moment bound.

The window, the grids, the scales and the cells are deterministic and fixed before the multiplier is read; that is the quantifier order below, in which the cell families are bound outside the almost-everywhere quantifier.

• measurable : Measurable Y
• one_le (a : CoeffSpace d) : 1 ≤ Y a
• standard_primal : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (k : ℤ) (w : Fin d → ℤ), standardCell d k w ⊆ centeredCube d M → BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (Y a * burnDiscount g jStar k) E)
• standard_adjoint : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (k : ℤ) (w : Fin d → ℤ), standardCell d k w ⊆ centeredCube d M → BlockMatLoewnerLE (coarseStarInv (standardCell d k w) a) (blockScale (Y a * burnDiscount g jStar k) (blockReflect E))
• adapted_primal : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (n : Mat d), Matrix.PosDef n → ∀ (r : ℤ) (y : Vec d), adaptedCellTranslate (roundedGrid jStar n) r y ⊆ centeredCube d M → BlockMatLoewnerLE (coarseBlock (adaptedCellTranslate (roundedGrid jStar n) r y) a) (blockScale (boundaryConst Cd g n * Y a * burnDiscount g jStar r) E)
• adapted_adjoint : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (n : Mat d), Matrix.PosDef n → ∀ (r : ℤ) (y : Vec d), adaptedCellTranslate (roundedGrid jStar n) r y ⊆ centeredCube d M → BlockMatLoewnerLE (coarseStarInv (adaptedCellTranslate (roundedGrid jStar n) r y) a) (blockScale (boundaryConst Cd g n * Y a * burnDiscount g jStar r) (blockReflect E))
• orlicz : IndependentSums.IsBigOWith P Ψ (fun (a : CoeffSpace d) => Y a - 1) (sourceRemainderScale d jStar K)
• lp_moment (p : ℝ) : 1 ≤ p → MeasureTheory.eLpNorm Y (ENNReal.ofReal p) P ≤ ENNReal.ofReal (1 + sourceRemainderScale d jStar K * momentMultiplier p (growthBar K))

The mixed source-tail relation

def HCPolySupport.HighContrast.IsShiftedBigOWith {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (Ψ : ℝ → ℝ) (X : CoeffSpace d → ℝ) (b c : ℝ) : Prop

The mixed source-tail relation X ≤ b + O_{Ψ_S}(c) of 02: almost surely X ≤ b + Z for a nonnegative Z with the weak-Orlicz tail at scale c.

Equations

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

def HCPolySupport.HighContrast.IsShiftedBigOWithTop {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (Ψ : ℝ → ℝ) (X : CoeffSpace d → ENNReal) (b c : ℝ) : Prop

The mixed source-tail relation for an extended-real-valued quantity, such as a supremum over an infinite cell family.

Equations

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

The below-start and cell-family suprema

noncomputable def HCPolySupport.HighContrast.belowStartSup {d : ℕ} (rho : ℝ) (q : Mat d) (jStar t : ℤ) (Z : ℤ → Set (Vec d)) (F : BlockMat d) (a : CoeffSpace d) : ENNReal

The below-start quantity S_{t,<j_*}(F) (the below-start source maximum): the weighted supremum, over the scales below the burn and the given below-start centers, of the size of the positive part of the F-normalized excess of the adapted response.

Equations

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

noncomputable def HCPolySupport.HighContrast.cellFamilyCenteredSup {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (Q : ℝ) (W : Set (Set (Vec d))) (F : BlockMat d) (a : CoeffSpace d) : ENNReal

The centered cell-family supremum sup_{W ∈ 𝒲} |F^{-1/2}(𝐀(W) - E[𝐀(W)])F^{-1/2}|_{S_Q}.

Equations

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

noncomputable def HCPolySupport.HighContrast.cellFamilyMeanSup {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (W : Set (Set (Vec d))) (F : BlockMat d) : ENNReal

The mean cell-family supremum sup_{W ∈ 𝒲} |F^{-1/2}E[𝐀(W)]F^{-1/2}|.

Equations

• HCPolySupport.HighContrast.cellFamilyMeanSup P W F = ⨆ V ∈ W, ENNReal.ofReal (HCPolySupport.HighContrast.blockSize (HCPolySupport.HighContrast.annealedBlock P V) F)

noncomputable def HCPolySupport.HighContrast.annealedStarInv {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (U : Set (Vec d)) : BlockMat d

The annealed sharp-adjoint block E[𝐀_*^{-1}(U;·)]. The sharp adjoint is the block reflection of the response, and the reflection permutes entries, so the expectation of the reflection is the reflection of the expectation.

Equations

• HCPolySupport.HighContrast.annealedStarInv P U = HCPolySupport.blockReflect (HCPolySupport.HighContrast.annealedBlock P U)

noncomputable def HCPolySupport.HighContrast.cellFamilyCenteredSupAdjoint {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (Q : ℝ) (W : Set (Set (Vec d))) (F : BlockMat d) (a : CoeffSpace d) : ENNReal

The sharp-adjoint centered cell-family supremum.

Equations

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

noncomputable def HCPolySupport.HighContrast.cellFamilyMeanSupAdjoint {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (W : Set (Set (Vec d))) (F : BlockMat d) : ENNReal

The sharp-adjoint mean cell-family supremum.

Equations

• HCPolySupport.HighContrast.cellFamilyMeanSupAdjoint P W F = ⨆ V ∈ W, ENNReal.ofReal (HCPolySupport.HighContrast.blockSize (HCPolySupport.HighContrast.annealedStarInv P V) F)

def HCPolySupport.HighContrast.IsAdmissibleIndex {d : ℕ} (q : Mat d) (jStar M r : ℤ) (w : Fin d → ℤ) : Prop

An admissible index for the grid q inside the window □_M: the scale is at or above the burn, the aligned cell at that scale and index is contained in the window, and so is the centered cell at that scale.

Equations

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

noncomputable def HCPolySupport.HighContrast.initGridConst {d : ℕ} (Cd g : ℝ) (E : BlockMat d) (mu : Mat d) : ℝ

The source constant of the window grid, K_q^S = κ_𝐄 B_q² 𝒰² with 𝒰 = 2.

Equations

• HCPolySupport.HighContrast.initGridConst Cd g E mu = HCPolySupport.HighContrast.kappaRef E * HCPolySupport.HighContrast.boundaryConst Cd g mu ^ 2 * 4

noncomputable def HCPolySupport.HighContrast.initIdentityConst {d : ℕ} (E : BlockMat d) : ℝ

The same constant on the identity grid, K_I^S = κ_𝐄 𝒰² = 4κ_𝐄.

Equations

• HCPolySupport.HighContrast.initIdentityConst E = 4 * HCPolySupport.HighContrast.kappaRef E

The bad scales of a window and their strict successor

def HCPolySupport.HighContrast.badScaleEvent {d : ℕ} (g : ℝ) (E : BlockMat d) (h m : ℤ) (a : CoeffSpace d) : Prop

The bad-scale event B_sans_{P,h}(m) of a window of height h: at generation m some standard aligned cube centered in □_m exceeds the reference block, after the discount 3^{-g(m-h-k)_+} at its own scale k.

Equations

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

noncomputable def HCPolySupport.HighContrast.successorScale {d : ℕ} (g : ℝ) (E : BlockMat d) (h : ℤ) (a : CoeffSpace d) : ENNReal

The strict successor of the last bad triadic scale, S_hat_{P,h} = 3 sup({3^m : B_sans_{P,h}(m) occurs} ∪ {0}). The empty supremum is zero, and the value is infinite exactly when the bad scales are unbounded above.

Equations

• HCPolySupport.HighContrast.successorScale g E h a = 3 * ⨆ (m : ℤ), ⨆ (_ : HCPolySupport.HighContrast.badScaleEvent g E h m a), ENNReal.ofReal (3 ^ m)

noncomputable def HCPolySupport.HighContrast.poweredGauge (Ψ : ℝ → ℝ) (g : ℝ) : ℝ → ℝ

The powered source gauge Ψ_S^{(g)}(t) = Ψ_S(t^{1/g}).

Equations

• HCPolySupport.HighContrast.poweredGauge Ψ g t = Ψ (t ^ g⁻¹)

noncomputable def HCPolySupport.HighContrast.poweredRemainderScale (d : ℕ) (jStar : ℤ) (g K : ℝ) : ℝ

The powered source-remainder scale ã_{j_*,g}^S = K_bar_S^{4g(d+1)}3^{g(2-j_*)}.

Equations

• HCPolySupport.HighContrast.poweredRemainderScale d jStar g K = HCPolySupport.HighContrast.growthBar K ^ (4 * g * (↑d + 1)) * 3 ^ (g * (2 - ↑jStar))