High-contrast homogenization: Entry.Source.AdaptedBound

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

From a successful source depth to adapted bounds

Near l.source.whitney. Dagger is used on a single event simultaneously for every integer source translate. Finer standard cells are assigned to their aligned ancestor, and coarser cells use the actual standard subdivision and source subadditivity.

theorem HCPolySupport.HighContrast.Source.source_finer_standard_bound {d : ℕ} (γ : ℝ) (E : BlockMat d) (S : CoeffSpace d → ℝ) (a : CoeffSpace d) (jStar r : ℕ) (hcoarse : ∀ (z : Fin d → ℤ) (m : ℤ), S (translateCoeff z a) ≤ 3 ^ m → ∀ k ≤ m, ∀ (w : Fin d → ℤ), standardCellCenter k w ∈ centeredCube d m → BlockMatLoewnerLE (coarseBlock (standardCell d k w) (translateCoeff z a)) (blockScale (3 ^ (γ * (↑m - ↑k))) E)) (hsuccess : ∀ (v : Fin d → ℤ), standardCellCenter (↑(jStar + r)) v ∈ centeredCube d ↑(2 * jStar + r) → S (translateCoeff (fun (i : Fin d) => 3 ^ (jStar + r) * v i) a) ≤ 3 ^ (jStar + r)) (k : ℤ) (w : Fin d → ℤ) (hkm : k ≤ ↑(jStar + r)) (hcell : standardCell d k w ⊆ centeredCube d (2 * ↑jStar)) : BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (3 ^ (γ * (↑(jStar + r) - ↑k))) E)

At a successful source offset, dagger controls every finer standard cell in the original window on the one simultaneous integer-translation event.

theorem HCPolySupport.HighContrast.Source.source_standard_bound {d : ℕ} [NeZero d] (γ : ℝ) (E : BlockMat d) (S : CoeffSpace d → ℝ) (a : CoeffSpace d) (jStar r : ℕ) (hcoarse : ∀ (z : Fin d → ℤ) (m : ℤ), S (translateCoeff z a) ≤ 3 ^ m → ∀ k ≤ m, ∀ (w : Fin d → ℤ), standardCellCenter k w ∈ centeredCube d m → BlockMatLoewnerLE (coarseBlock (standardCell d k w) (translateCoeff z a)) (blockScale (3 ^ (γ * (↑m - ↑k))) E)) (hsuccess : ∀ (v : Fin d → ℤ), standardCellCenter (↑(jStar + r)) v ∈ centeredCube d ↑(2 * jStar + r) → S (translateCoeff (fun (i : Fin d) => 3 ^ (jStar + r) * v i) a) ≤ 3 ^ (jStar + r)) (k : ℤ) (w : Fin d → ℤ) (hcell : standardCell d k w ⊆ centeredCube d (2 * ↑jStar)) : BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (3 ^ (γ * max (↑(jStar + r) - ↑k) 0)) E)

Standard-cell subdivision extends the successful-depth estimate to every generation, including coarser cells, with the printed positive part and no geometric factor.

theorem HCPolySupport.HighContrast.Source.source_penalty_decay (γ J j r : ℝ) (hγ : 0 ≤ γ) (hr : r ≤ j) : 3 ^ (r - j) * 3 ^ (γ * max (J - r) 0) ≤ 3 ^ (γ * max (J - j) 0) * 3 ^ ((1 - γ) * (r - j))

The positive-part source penalty combines with boundary-layer decay geometrically.

theorem HCPolySupport.HighContrast.Source.source_whitney_weighted_sum {d : ℕ} [NeZero d] {q : Mat d} (hq : Geometry.InverseNormLE q 2) (j : ℤ) (y : Vec d) (J : ℕ) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : have W := adaptedCellTranslate q j y; have s := Geometry.maximalCellPairs W j; (Summable fun (t : ↑s) => (MeasureTheory.volume (standardCell d (↑t).1 (↑t).2)).toReal / (MeasureTheory.volume W).toReal * 3 ^ (γ * max (↑J - ↑(↑t).1) 0)) ∧ ∑' (t : ↑s), (MeasureTheory.volume (standardCell d (↑t).1 (↑t).2)).toReal / (MeasureTheory.volume W).toReal * 3 ^ (γ * max (↑J - ↑(↑t).1) 0) ≤ 12 * ↑d ^ (3 / 2) * 3 ^ (γ * max (↑J - ↑j) 0) / (1 - 3 ^ (-(1 - γ)))

The full Whitney series has a summable source penalty, with the exact geometric ratio. Reindexing by the nonnegative deficit retains every selected cell.

theorem HCPolySupport.HighContrast.Source.source_penalty_factor (γ : ℝ) (hγ : 0 ≤ γ) (J r : ℕ) (k : ℤ) : 3 ^ (γ * max (↑(J + r) - ↑k) 0) ≤ 3 ^ (γ * ↑r) * 3 ^ (γ * max (↑J - ↑k) 0)

Separating the least offset retains the factor-one standard bound at every integer scale, including scales below the source window.

theorem HCPolySupport.HighContrast.Source.adapted_bound_of_standard {d : ℕ} [NeZero d] (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (E : BlockMat d) (hE : Book.Ch02.BlockPosDef E) (a : CoeffSpace d) (J : ℕ) (X : ℝ) (hX : 0 ≤ X) (hstd : ∀ (k : ℤ) (w : Fin d → ℤ), standardCell d k w ⊆ centeredCube d (2 * ↑J) → BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (X * 3 ^ (γ * max (↑J - ↑k) 0)) E)) {q : Mat d} (hq : Geometry.InverseNormLE q 2) (j : ℤ) (y : Vec d) (hcell : adaptedCellTranslate q j y ⊆ centeredCube d (2 * ↑J)) : BlockMatLoewnerLE (coarseBlock (adaptedCellTranslate q j y) a) (blockScale (12 * ↑d ^ (3 / 2) / (1 - 3 ^ (-(1 - γ))) * X * 3 ^ (γ * max (↑J - ↑j) 0)) E)

One simultaneous standard bound controls every contained adapted cell. The full countable partition is assembled through the mixed response identity.

theorem HCPolySupport.HighContrast.Source.source_standard_multiplier_bound {d : ℕ} [NeZero d] (γ : ℝ) (E : BlockMat d) (hγ : 0 ≤ γ) (hE : Book.Ch02.BlockPosDef E) (S : CoeffSpace d → ℝ) (a : CoeffSpace d) (jStar r : ℕ) (hcoarse : ∀ (z : Fin d → ℤ) (m : ℤ), S (translateCoeff z a) ≤ 3 ^ m → ∀ k ≤ m, ∀ (w : Fin d → ℤ), standardCellCenter k w ∈ centeredCube d m → BlockMatLoewnerLE (coarseBlock (standardCell d k w) (translateCoeff z a)) (blockScale (3 ^ (γ * (↑m - ↑k))) E)) (hsuccess : ∀ (v : Fin d → ℤ), standardCellCenter (↑(jStar + r)) v ∈ centeredCube d ↑(2 * jStar + r) → S (translateCoeff (fun (i : Fin d) => 3 ^ (jStar + r) * v i) a) ≤ 3 ^ (jStar + r)) (k : ℤ) (w : Fin d → ℤ) (hcell : standardCell d k w ⊆ centeredCube d (2 * ↑jStar)) : BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (3 ^ (γ * ↑r) * 3 ^ (γ * max (↑jStar - ↑k) 0)) E)

The same attained source value gives the printed factor-one standard-cell estimate.

theorem HCPolySupport.HighContrast.Source.one_le_source_eccentricity {d : ℕ} [NeZero d] {m : Mat d} (hm : Matrix.PosDef m) : 1 ≤ √(‖m‖ * ‖m⁻¹‖)

The printed eccentricity is at least one for a positive metric in nonzero dimension.

theorem HCPolySupport.HighContrast.Source.source_multiplier_and_adapted_bound (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ) (C : ℝ), 0 < Csrc ∧ 0 < C ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), IsStationaryLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → have Good := fun (r : ℕ) (a : CoeffSpace d) => ∀ (w : Fin d → ℤ), standardCellCenter (↑(jStar + r)) w ∈ centeredCube d ↑(2 * jStar + r) → S (translateCoeff (fun (i : Fin d) => 3 ^ (jStar + r) * w i) a) ≤ 3 ^ (jStar + r); ∃ (ell : CoeffSpace d → ℕ) (X : CoeffSpace d → ℝ), Measurable ell ∧ Measurable X ∧ (∀ (a : CoeffSpace d), X a = 3 ^ (γ * ↑(ell a))) ∧ (∀ᵐ (a : CoeffSpace d) ∂P, Good (ell a) a ∧ (∀ (r : ℕ), Good r a → ell a ≤ r) ∧ ∀ (r : ℕ), Good r a → X a ≤ 3 ^ (γ * ↑r)) ∧ MeasureTheory.MemLp X (ENNReal.ofReal ↑(bigQ d γ)) P ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => X a ^ bigQ d γ) P ∧ ∫ (a : CoeffSpace d), X a ^ bigQ d γ ∂P ≤ 2 ^ bigQ d γ ∧ MeasureTheory.eLpNorm X (ENNReal.ofReal ↑(bigQ d γ)) P ≤ ENNReal.ofReal 2 ∧ ∀ᵐ (a : CoeffSpace d) ∂P, (∀ (k : ℤ) (w : Fin d → ℤ), standardCell d k w ⊆ centeredCube d (2 * ↑jStar) → BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (X a * 3 ^ (γ * max (↑jStar - ↑k) 0)) E)) ∧ ∀ (m : Mat d), Matrix.PosDef m → ∀ (j : ℤ) (y : Vec d), adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j y ⊆ centeredCube d (2 * ↑jStar) → BlockMatLoewnerLE (coarseBlock (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j y) a) (blockScale (C * √(‖m‖ * ‖m⁻¹‖) * X a * 3 ^ (γ * max (↑jStar - ↑j) 0)) E)

The characterized source multiplier, its fixed-Q norm, and one simultaneous standard/adapted event. Both constants are chosen before all source laws and data.