High-contrast homogenization: Entry.Annealed.TransportDriftComparison

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

Transport drift comparison on two rounded grids

The deterministic drift estimates consumed by the two-grid transport. The module proves the scaling-composition law blockScale a (blockScale b A) = blockScale (a * b) A and a cross-source comparison bounding the annealed mean of one rounded grid by a constant multiple of the annealed mean of a second rounded grid. It then removes the temporary source-scale cap from the maximal-family partition comparison, assembles the complete Whitney drift comparison, and deduces the printed determinant-drift estimate: on two positive definite geometries within bounded projective distance, the drift of the transported geometry is bounded by the scaled drift of the reference geometry plus the partition, source and terminal-decay terms. These estimates serve Proposition p.two.grid.transport.

theorem HCPolySupport.HighContrast.Annealed.transport_scale_scale {d : ℕ} (a b : ℝ) (A : BlockMat d) : blockScale a (blockScale b A) = blockScale (a * b) A

Scaling twice multiplies the real coefficients.

theorem HCPolySupport.HighContrast.Annealed.exists_transport_cross_source_mean (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 → ∀ (m mPlus : Mat d), Matrix.PosDef m → Matrix.PosDef mPlus → ∀ (s j : ℤ), ↑jStar ≤ s → ↑jStar ≤ j → adaptedCell (Geometry.explicitRoundedGrid jStar m) s ⊆ centeredCube d (2 * ↑jStar) → adaptedCell (Geometry.explicitRoundedGrid jStar mPlus) j ⊆ centeredCube d (2 * ↑jStar) → BlockMatLoewnerLE (adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) j) (blockScale (C * aspectRatio E * √(‖m‖ * ‖m⁻¹‖) * √(‖mPlus‖ * ‖mPlus⁻¹‖)) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) s))

Source normalization compares means on either rounded geometry, with a single outer constant.

theorem HCPolySupport.HighContrast.Annealed.transport_drift_subrow {d : ℕ} (W : Set (Vec d)) (q : Mat d) (hq : IsUnit q) (cap r : ℤ) (hfin : (maximalAdaptedCellCenters W q cap r).Finite) : let I := { p : ℤ × (Fin d → ℤ) // IsMaximalAdaptedCellIn W q cap p.1 p.2 }; ∑' (p : { p : { p : I // (↑p).1 < cap } // (↑↑p).1 = r }), (MeasureTheory.volume (adaptedCellAtCenter q (↑↑↑p).1 (↑↑↑p).2)).toReal / (MeasureTheory.volume W).toReal ≤ ∑ _z ∈ hfin.toFinset, (MeasureTheory.volume (adaptedCell q r)).toReal / (MeasureTheory.volume W).toReal

Removing the cap from a maximal-family row cannot increase its mass.

theorem HCPolySupport.HighContrast.Annealed.exists_transport_drift_partition_raw (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (K₀ : ℝ) (hK₀ : 1 ≤ K₀) : ∃ (Csrc : ℝ) (Cw : ℝ) (Ct : ℝ), 0 < Csrc ∧ 0 < Cw ∧ 0 < Ct ∧ ∀ (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 → ∀ (m mPlus : Mat d), Matrix.PosDef m → Matrix.PosDef mPlus → gridRatio (Geometry.explicitRoundedGrid jStar m) (Geometry.explicitRoundedGrid jStar mPlus) ≤ K₀ → ∀ (j terminal : ℤ), ↑jStar ≤ terminal → ∀ (L : ℕ), 1 ≤ L → ↑jStar ≤ j - ↑L → adaptedCell (Geometry.explicitRoundedGrid jStar mPlus) j ⊆ centeredCube d (2 * ↑jStar) → adaptedCell (Geometry.explicitRoundedGrid jStar m) terminal ⊆ centeredCube d (2 * ↑jStar) → BlockMatLoewnerLE (blockSub (adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) j) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (j - ↑L))) (ofFullBlockMat (Cw • ∑ r ∈ Finset.Icc (↑jStar) (max (↑jStar) (j - ↑L - 1)), 3 ^ (↑r - ↑j) • toFullBlockMat (adaptedMean P (Geometry.explicitRoundedGrid jStar m) r) + (Ct * Cw * aspectRatio E * √(‖m‖ * ‖m⁻¹‖) ^ 2 * 3 ^ (-(↑j - ↑jStar))) • toFullBlockMat (adaptedMean P (Geometry.explicitRoundedGrid jStar m) terminal)))

Apply the accepted partition comparison to the actual forward Whitney family. The temporary maximum in the summation cap isolates the source-scale endpoint.

theorem HCPolySupport.HighContrast.Annealed.transport_drift_cap_sum (J b j : ℤ) (hJb : J ≤ b) (f : ℤ → ℝ) (hfJ : 0 ≤ f J) : ∑ r ∈ Finset.Icc J (max J (b - 1)), 3 ^ (↑r - ↑j) * f r ≤ ∑ r ∈ Finset.Icc J (b - 1), 3 ^ (↑r - ↑j) * f r + 3 ^ (-(↑j - ↑J)) * f J

The temporary cap adds only the source-scale term, even at the first target generation.

theorem HCPolySupport.HighContrast.Annealed.transport_drift_partition_enlarge {d : ℕ} (A : ℤ → BlockMat d) (H F : BlockMat d) (hAJ : ∀ (r : ℤ), Matrix.PosSemidef (toFullBlockMat (A r))) (hF : Matrix.PosSemidef (toFullBlockMat F)) (J b j : ℤ) (hJb : J ≤ b) (hJj : J ≤ j) (Cw Cf M C D B γ : ℝ) (hCw : 0 ≤ Cw) (hCf : 0 ≤ Cf) (hM : 0 ≤ M) (hγ : 0 ≤ γ) (hcoeff : Cw * M + Cf ≤ D * B) (hCW : Cw ≤ C) (hsource : BlockMatLoewnerLE (A J) (blockScale M F)) (hraw : BlockMatLoewnerLE (blockSub H (A b)) (ofFullBlockMat (Cw • ∑ r ∈ Finset.Icc J (max J (b - 1)), 3 ^ (↑r - ↑j) • toFullBlockMat (A r) + (Cf * 3 ^ (-(↑j - ↑J))) • toFullBlockMat F))) : BlockMatLoewnerLE H (ofFullBlockMat (toFullBlockMat (A b) + C • ∑ r ∈ Finset.Icc J (b - 1), 3 ^ (↑r - ↑j) • toFullBlockMat (A r) + (D * B * 3 ^ (-(1 - γ) * (↑j - ↑J))) • toFullBlockMat F))

Remove the temporary source-scale cap and weaken only the scalar source decay.

theorem HCPolySupport.HighContrast.Annealed.exists_transport_whitney_drift_comparison (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (K₀ : ℝ) (hK₀ : 1 ≤ K₀) : ∃ (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 → ∀ (m mPlus : Mat d), Matrix.PosDef m → Matrix.PosDef mPlus → gridRatio (Geometry.explicitRoundedGrid jStar m) (Geometry.explicitRoundedGrid jStar mPlus) ≤ K₀ → ∀ (j terminal : ℤ), ↑jStar ≤ terminal → ∀ (L : ℕ), 1 ≤ L → ↑jStar ≤ j - ↑L → adaptedCell (Geometry.explicitRoundedGrid jStar mPlus) j ⊆ centeredCube d (2 * ↑jStar) → adaptedCell (Geometry.explicitRoundedGrid jStar m) terminal ⊆ centeredCube d (2 * ↑jStar) → BlockMatLoewnerLE (adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) j) (ofFullBlockMat (toFullBlockMat (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (j - ↑L)) + (C * K₀) • ∑ r ∈ Finset.Icc (↑jStar) (j - ↑L - 1), 3 ^ (↑r - ↑j) • toFullBlockMat (adaptedMean P (Geometry.explicitRoundedGrid jStar m) r) + (C * (1 + aspectRatio E * (√(‖m‖ * ‖m⁻¹‖) + √(‖mPlus‖ * ‖mPlus⁻¹‖)) ^ 2) * 3 ^ (-(1 - γ) * (↑j - ↑jStar))) • toFullBlockMat (adaptedMean P (Geometry.explicitRoundedGrid jStar m) terminal)))

The complete Whitney drift comparison, including the empty boundary at j=jStar+L.

theorem HCPolySupport.HighContrast.Annealed.exists_two_grid_drift_comparison (d : ℕ) (hd : 2 ≤ d) (K₀ : ℝ) (hK₀ : 1 ≤ K₀) (γ : ℝ) (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 → ∀ (m mPlus : Mat d), Matrix.PosDef m → Matrix.PosDef mPlus → gridRatio (Geometry.explicitRoundedGrid jStar m) (Geometry.explicitRoundedGrid jStar mPlus) ≤ K₀ → ∀ (n : ℤ), ↑jStar ≤ n → ∀ (L : ℕ), 1 ≤ L → adaptedCell (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L) ∪ adaptedCell (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L) ⊆ centeredCube d (2 * ↑jStar) → ∀ δ ∈ Set.Icc 0 (1 / 4), BlockMatLoewnerLE (blockScale (1 - δ) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L))) (adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L)) → BlockMatLoewnerLE (adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L)) (blockScale (1 + δ) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L))) → determinantDrift P γ (Geometry.explicitRoundedGrid jStar mPlus) jStar (n + ↑L) ≤ C * (δ + K₀ * 3 ^ (-↑L) + 3 ^ ((1 - γ) / 4 * ↑L) * determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + 2 * ↑L)) + C * (1 + aspectRatio E * (√(‖m‖ * ‖m⁻¹‖) + √(‖mPlus‖ * ‖mPlus⁻¹‖)) ^ 2) * (1 + ↑n + ↑L - ↑jStar) * 3 ^ (-((1 - γ) / 8) * (↑n - ↑jStar))

The complete printed determinant-drift estimate. The uniform errors use the mass-one Abel identity; the source term retains its linear scale factor.