High-contrast homogenization: Entry.Annealed.TransportDrift

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

Geometric drift weights for the two-grid transport

The drift estimates that the source and boundary corrections of the two-grid transport p.two.grid.transport consume: the boundary mean loses only the quarter-(1 - γ) power in the generation distance; the geometric convolutions of the fine source and of the comparison error have bounded mass; the early and fine weight sums keep the printed terminal decay; and the asymmetric profile bracket absorbs each source amplitude. One nonnegative source field, with L^Q norm and Q-th moment bounded independently of the law, the geometry and the generation choices, dominates the actual Whitney rows; the bulk fluctuations and the fluctuation history are reindexed as a single finite joint maximum over paired generations and centres, and the centered and mean reductions of the Whitney estimate are discharged with the source, positivity, series and moment guards.

theorem HCPolySupport.HighContrast.Annealed.transport_boundary_mean_bound (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (k n : ℤ) (hk : ↑jStar ≤ k) (hkn : k ≤ n) (L : ℕ) (hL : 1 ≤ L) : have q := Geometry.explicitRoundedGrid jStar m; have ell := fun (j : ℤ) => if j ≤ k + ↑L then 1 else L; ∑ j ∈ Finset.Icc (↑jStar + ↑L) (n + ↑L), 3 ^ (-((1 - γ) / 4) * (↑n + ↑L - 1 - ↑j)) * ∑ r ∈ Finset.Icc (↑jStar) (j - ↑(ell j) - 1), 3 ^ (-(1 - γ) * (↑j - ↑r)) * meanPenalty (bigQ d γ) (relMean P q r (n + 2 * ↑L)) ≤ 1 / (1 - 3 ^ (-(3 / 4 * (1 - γ)))) * (2 + 1 / (1 - 3 ^ (-((1 - γ) / 4)))) * 3 ^ ((1 - γ) / 4 * ↑L) * profile P γ q jStar k (n + 2 * ↑L)

The actual boundary mean sum has only the quarter-(1-gamma) loss in L.

theorem HCPolySupport.HighContrast.Annealed.transport_source_convolution (a b : ℝ) (hab : a < b) (J lo t : ℤ) (hlo : J ≤ lo) : ∑ j ∈ Finset.Icc lo t, 3 ^ (-a * (↑t - ↑j)) * 3 ^ (-b * (↑j - ↑J)) ≤ 1 / (1 - 3 ^ (-(b - a))) * 3 ^ (-a * (↑t - ↑J))

A source convolution retains its terminal decay and has a geometric mass.

theorem HCPolySupport.HighContrast.Annealed.transport_fine_weight_sum (γ : ℝ) (hγ : γ < 1) (Q : ℕ) (hQ : 1 ≤ Q) (J n : ℤ) (L : ℕ) : ∑ j ∈ Finset.Icc (J + ↑L) (n + ↑L), 3 ^ (-((1 - γ) / 4) * (↑n + ↑L - ↑j)) * (3 ^ (-(1 - γ) * (↑j - ↑J)) + 3 ^ (-↑Q * (1 - γ) * (↑j - ↑J))) ≤ 2 / (1 - 3 ^ (-(3 * (1 - γ) / 4))) * 3 ^ (-((1 - γ) / 4) * (↑n + ↑L - ↑J))

Both fine-source powers have the printed decay, including an empty target range.

theorem HCPolySupport.HighContrast.Annealed.transport_early_weight_sum (a : ℝ) (ha : 0 < a) (J n : ℤ) (L : ℕ) : ∑ j ∈ Finset.Icc J (J + ↑L - 1), 3 ^ (-a * (↑n + ↑L - ↑j)) ≤ 1 / (1 - 3 ^ (-a)) * 3 ^ (-a * (↑n - ↑J))

Early target generations start at J and pay decay in n−J.

theorem HCPolySupport.HighContrast.Annealed.transport_comparison_error_sum (a : ℝ) (ha : 0 < a) (J t : ℤ) (δ : ℝ) (hδ : 0 ≤ δ) : ∑ j ∈ Finset.Icc J t, 3 ^ (-a * (↑t - ↑j)) * δ ≤ 1 / (1 - 3 ^ (-a)) * δ

The comparison error has bounded geometric mass.

theorem HCPolySupport.HighContrast.Annealed.transport_profile_source_bracket {Pi K₀ e ePlus : ℝ} (hPi : 0 ≤ Pi) (hK₀ : 0 ≤ K₀) (he : 0 ≤ e) (hePlus : 0 ≤ ePlus) : 1 ≤ 1 + Pi * (K₀ * e * ePlus + ePlus ^ 2) ∧ Pi * K₀ * e * ePlus ≤ 1 + Pi * (K₀ * e * ePlus + ePlus ^ 2) ∧ Pi * ePlus ^ 2 ≤ 1 + Pi * (K₀ * e * ePlus + ePlus ^ 2)

The asymmetric profile bracket absorbs each of its source amplitudes.

theorem HCPolySupport.HighContrast.Annealed.exists_transport_target_source (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 → ∃ (X : CoeffSpace d → ℝ), (∀ (a : CoeffSpace d), 0 ≤ X a) ∧ MeasureTheory.MemLp X (ENNReal.ofReal ↑(bigQ d γ)) P ∧ MeasureTheory.eLpNorm X (ENNReal.ofReal ↑(bigQ d γ)) P ≤ ENNReal.ofReal 2 ∧ MeasureTheory.Integrable X P ∧ ∫ (a : CoeffSpace d), X a ∂P ≤ 2 ∧ ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (mPlus : Mat d), Matrix.PosDef mPlus → ∀ (s : ℤ), ↑jStar ≤ s → adaptedCell (Geometry.explicitRoundedGrid jStar mPlus) s ⊆ centeredCube d (2 * ↑jStar) → ∀ (j : ℤ), ↑jStar ≤ j → ∀ (y : Vec d), adaptedCellTranslate (Geometry.explicitRoundedGrid jStar mPlus) j y ⊆ centeredCube d (2 * ↑jStar) → BlockMatLoewnerLE (normalizedBlock (coarseBlock (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar mPlus) j y) a) (adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) s)) (blockScale (C * aspectRatio E * √(‖mPlus‖ * ‖mPlus⁻¹‖) ^ 2 * X a) (Book.Ch02.blockIdentity d))

Applying the source theorem to the target itself gives the square of the new-grid eccentricity. One X works for all target generations and centers.

theorem HCPolySupport.HighContrast.Annealed.transport_source_moment {α : Type u_1} [MeasurableSpace α] {P : MeasureTheory.Measure α} (Q : ℕ) (hQ : 0 < Q) (X : α → ℝ) (hX0 : ∀ᵐ (a : α) ∂P, 0 ≤ X a) (hX : MeasureTheory.MemLp X (ENNReal.ofReal ↑Q) P) (M : ℝ) (hM : 0 ≤ M) (hnorm : MeasureTheory.eLpNorm X (ENNReal.ofReal ↑Q) P ≤ ENNReal.ofReal M) : ∫ (a : α), X a ^ Q ∂P ≤ M ^ Q

The source L^Q bound gives its actual Bochner moment.

theorem HCPolySupport.HighContrast.Annealed.transport_source_sum_moment {α : Type u_1} [MeasurableSpace α] {P : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure P] (Q : ℕ) (hQ : 0 < Q) (X Y : α → ℝ) (hX0 : ∀ᵐ (a : α) ∂P, 0 ≤ X a) (hY0 : ∀ᵐ (a : α) ∂P, 0 ≤ Y a) (hX : MeasureTheory.MemLp X (ENNReal.ofReal ↑Q) P) (hY : MeasureTheory.MemLp Y (ENNReal.ofReal ↑Q) P) (hXN : MeasureTheory.eLpNorm X (ENNReal.ofReal ↑Q) P ≤ ENNReal.ofReal 2) (hYN : MeasureTheory.eLpNorm Y (ENNReal.ofReal ↑Q) P ≤ ENNReal.ofReal 2) : ∫ (a : α), (X a + Y a + 4) ^ Q ∂P ≤ 3 ^ Q * (2 * 2 ^ Q + 4 ^ Q)

Two common source fields and their centering constants have a fixed moment.

theorem HCPolySupport.HighContrast.Annealed.transport_source_max_weight (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (J n j : ℤ) (L : ℕ) (_hn : J ≤ n) (hj : j ∈ Set.Icc J (n + ↑L)) : have b := (1 - γ) / 4 / ↑(bigQ d γ); (j < J + ↑L → 3 ^ (-rhoMax d γ * (↑n + ↑L - ↑j)) ≤ 3 ^ (-b * (↑n - ↑J))) ∧ 3 ^ (-rhoMax d γ * (↑n + ↑L - ↑j)) * 3 ^ (-(1 - γ) * (↑j - ↑J)) ≤ 3 ^ (-b * (↑n - ↑J)) ∧ (3 ^ (-b * (↑n - ↑J))) ^ bigQ d γ = 3 ^ (-((1 - γ) / 4) * (↑n - ↑J))

Both early targets and fine Whitney tails pay a single common source weight; raising that weight to Q gives exactly the printed profile decay.

theorem HCPolySupport.HighContrast.Annealed.exists_transport_bulk_fluctuations (d : ℕ) (hd : 2 ≤ d) (K₀ : ℝ) (hK₀ : 1 ≤ K₀) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m mPlus : Mat d), Matrix.PosDef m → Matrix.PosDef mPlus → gridRatio (Geometry.explicitRoundedGrid jStar m) (Geometry.explicitRoundedGrid jStar mPlus) ≤ K₀ → ∀ (k n : ℤ), ↑jStar ≤ k → k ≤ n → ∀ (L : ℕ), 1 ≤ L → have q := Geometry.explicitRoundedGrid jStar m; have qPlus := Geometry.explicitRoundedGrid jStar mPlus; have Q := bigQ d γ; have ell := fun (j : ℤ) => if j ≤ k + ↑L then 1 else L; have cap := fun (j : ℤ) => j - ↑(ell j); have W := fun (p : ℤ × (Fin d → ℤ)) => adaptedCellAtCenter qPlus p.1 p.2; ∀ (I : Finset (ℤ × (Fin d → ℤ))), (∀ p ∈ I, p.1 ∈ Set.Icc (↑jStar + ↑L) (n + ↑L)) → (∀ p ∈ I, standardCellCenter p.1 p.2 ∈ centeredCube d (n + ↑L)) → ∃ (hfin : ∀ (p : ℤ × (Fin d → ℤ)), ∀ r ≤ cap p.1, (maximalAdaptedCellCenters (W p) q (cap p.1) r).Finite), have Z := fun (p : ℤ × (Fin d → ℤ)) => ⋯.toFinset; have v := fun (p : ℤ × (Fin d → ℤ)) => (MeasureTheory.volume (adaptedCell q (cap p.1))).toReal / (MeasureTheory.volume (W p)).toReal; ∫ (a : CoeffSpace d), (⨆ p ∈ ↑I, 3 ^ (-rhoMax d γ * (↑n + ↑L - ↑p.1)) * absSchattenNorm (↑Q) (ofFullBlockMat (∑ z ∈ Z p, v p • toFullBlockMat (normalizedFluctuation P q (cap p.1) (n + 2 * ↑L) z a)))) ^ ↑Q ∂P ≤ C * 3 ^ ((1 - γ) / 4 * ↑L) * profile P γ q jStar k (n + 2 * ↑L)

The printed bulk fluctuation estimate for the actual Whitney rows. The constant precedes the law, geometry and all generation choices.

theorem HCPolySupport.HighContrast.Annealed.transport_fluctuation_history_reindex {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (q : Mat d) (hq : IsUnit q) (jStar : ℕ) (t : ℤ) (ht : ↑jStar ≤ t) : ∃ (I : Finset (ℤ × (Fin d → ℤ))), I.Nonempty ∧ (∀ (p : ℤ × (Fin d → ℤ)), p ∈ I ↔ p.1 ∈ Set.Icc (↑jStar) t ∧ standardCellCenter p.1 p.2 ∈ centeredCube d t) ∧ fluctuationHistory P γ q jStar t = ∫ (a : CoeffSpace d), (⨆ p ∈ ↑I, 3 ^ (-rhoMax d γ * (↑t - ↑p.1)) * blockOpNorm (normalizedFluctuation P q p.1 t (adaptedCellCenter q p.1 p.2) a)) ^ ↑(bigQ d γ) ∂P

The real fluctuation history is exactly one finite joint maximum over paired target generations and integer centers, with its Q-th power outside.

theorem HCPolySupport.HighContrast.Annealed.exists_transport_whitney_reduction (d : ℕ) (hd : 2 ≤ d) (K₀ : ℝ) (hK₀ : 1 ≤ K₀) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ) (Cf : ℝ) (Cm : ℝ), 0 < Csrc ∧ 0 < Cf ∧ 0 < Cm ∧ ∀ (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 → ∃ (X : CoeffSpace d → ℝ), (∀ (a : CoeffSpace d), 0 ≤ X a) ∧ MeasureTheory.MemLp X (ENNReal.ofReal ↑(bigQ d γ)) P ∧ MeasureTheory.eLpNorm X (ENNReal.ofReal ↑(bigQ d γ)) P ≤ ENNReal.ofReal 2 ∧ MeasureTheory.Integrable X P ∧ ∫ (a : CoeffSpace d), X a ∂P ≤ 2 ∧ ∀ (m mPlus : Mat d), Matrix.PosDef m → Matrix.PosDef mPlus → gridRatio (Geometry.explicitRoundedGrid jStar m) (Geometry.explicitRoundedGrid jStar mPlus) ≤ K₀ → ∀ (oldEnd newEnd j : ℤ), j ≤ newEnd → ∀ (ell : ℕ), 1 ≤ ell → ↑jStar ≤ j - ↑ell → j - ↑ell ≤ oldEnd → adaptedCell (Geometry.explicitRoundedGrid jStar mPlus) newEnd ⊆ centeredCube d (2 * ↑jStar) → ∀ (w : Fin d → ℤ), standardCellCenter j w ∈ centeredCube d newEnd → ∀ δ ∈ Set.Icc 0 (1 / 4), have q := Geometry.explicitRoundedGrid jStar m; have qPlus := Geometry.explicitRoundedGrid jStar mPlus; have Q := bigQ d γ; have cap := j - ↑ell; have W := adaptedCellAtCenter qPlus j w; have B := aspectRatio E * K₀ * √(‖m‖ * ‖m⁻¹‖) * √(‖mPlus‖ * ‖mPlus⁻¹‖); have decay := 3 ^ (-(1 - γ) * (↑j - ↑jStar)); have F := adaptedMean P q oldEnd; have H := adaptedMean P qPlus newEnd; let I := { p : ℤ × (Fin d → ℤ) // IsMaximalAdaptedCellIn W q cap p.1 p.2 }; have f := fun (p : I) (a : CoeffSpace d) => ⋯ • ⋯; have G := fun (a : CoeffSpace d) => ⋯; have MG := ⋯; ⋯

The centered and mean reductions with every Whitney, source, positivity, series and moment guard discharged. The same source X serves all targets.