High-contrast homogenization: Entry.Annealed.TransportProfileComparison

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

Profile comparison for the two-grid transport

This module proves the profile comparison behind p.two.grid.transport. It bounds the joint maximum of a common source envelope and two fluctuation envelopes by three scalar moments, with no factor for the number of targets or generations; pays the actual lattice count on the target range through the mean-decay gap; records the weighted mean-history convention with its fixed factor 3^{(1−γ)/4}; accumulates the bulk and boundary means, the comparison error and both source powers while keeping the early target range separate; and shows that a source bound on an actual target controls both its centered matrix and its deterministic mean penalty at the same geometric amplitude. The resulting printed estimate compares the profiles of two geometries within projective distance and Loewner-close annealed blocks, at the growth 3^{(1−γ)L/2}, the comparison error and the determinant drift of the transported geometry, with the two source amplitudes kept separate.

theorem HCPolySupport.HighContrast.Annealed.transport_joint_three_envelopes {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {P : MeasureTheory.Measure α} (Q : ℕ) (hQ : 0 < Q) (I : Finset ι) (hI : I.Nonempty) (f : ι → α → ℝ) (hf0 : ∀ i ∈ I, ∀ᵐ (a : α) ∂P, 0 ≤ f i a) (hf : ∀ i ∈ I, MeasureTheory.MemLp (f i) (ENNReal.ofReal ↑Q) P) (X Y Z : α → ℝ) (hX0 : ∀ᵐ (a : α) ∂P, 0 ≤ X a) (hY0 : ∀ᵐ (a : α) ∂P, 0 ≤ Y a) (hZ0 : ∀ᵐ (a : α) ∂P, 0 ≤ Z a) (hX : MeasureTheory.MemLp X (ENNReal.ofReal ↑Q) P) (hY : MeasureTheory.MemLp Y (ENNReal.ofReal ↑Q) P) (hZ : MeasureTheory.MemLp Z (ENNReal.ofReal ↑Q) P) (A D : ℝ) (hA : 0 ≤ A) (hD : 0 ≤ D) (hbound : ∀ i ∈ I, ∀ᵐ (a : α) ∂P, f i a ≤ A * (X a + Y a) + D * Z a) : ∫ (a : α), (⨆ i ∈ ↑I, f i a) ^ ↑Q ∂P ≤ 3 ^ Q * (A ^ Q * (∫ (a : α), X a ^ Q ∂P + ∫ (a : α), Y a ^ Q ∂P) + D ^ Q * ∫ (a : α), Z a ^ Q ∂P)

A common source envelope and two fluctuation maxima combine with three scalar moments. There is no factor for the number of targets or generations.

theorem HCPolySupport.HighContrast.Annealed.transport_pair_mean_bound (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (I : Finset (ℤ × (Fin d → ℤ))) (J t : ℤ) (hgen : ∀ p ∈ I, p.1 ∈ Set.Icc J t) (hcenter : ∀ p ∈ I, standardCellCenter p.1 p.2 ∈ centeredCube d t) (M : ℤ × (Fin d → ℤ) → ℝ) (B : ℤ → ℝ) (hB : ∀ j ∈ Finset.Icc J t, 0 ≤ B j) (hM : ∀ p ∈ I, M p ≤ B p.1) : ∑ p ∈ I, (3 ^ (-rhoMax d γ * (↑t - ↑p.1))) ^ ↑(bigQ d γ) * M p ≤ ∑ j ∈ Finset.Icc J t, 3 ^ (-((1 - γ) / 4) * (↑t - ↑j)) * B j

The deterministic target sum pays the actual lattice count, then uses Qρ−d ≥ (1−γ)/4. Only this mean term is summed over the target cells.

theorem HCPolySupport.HighContrast.Annealed.transport_meanHistory_weighted_bound {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (q : Mat d) (J t : ℤ) (B : ℤ → ℝ) (hB : ∀ j ∈ Finset.Icc J t, 0 ≤ B j) (hM : ∀ j ∈ Finset.Ico J t, meanPenalty (bigQ d γ) (relMean P q j t) ≤ B j) : meanHistory P γ q J t ≤ 3 ^ ((1 - γ) / 4) * ∑ j ∈ Finset.Icc J t, 3 ^ (-((1 - γ) / 4) * (↑t - ↑j)) * B j

The mean-history convention uses t−1−j; its extra fixed factor is 3^a.

theorem HCPolySupport.HighContrast.Annealed.transport_weighted_mean_accumulation (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) (Cm Ce δ B : ℝ) (hCm : 0 ≤ Cm) (hCe : 0 ≤ Ce) (hδ : 0 ≤ δ) (hB : 0 ≤ B) : have q := Geometry.explicitRoundedGrid jStar m; have Q := bigQ d γ; have a := (1 - γ) / 4; have G₁ := 1 / (1 - 3 ^ (-a)); have G₃ := 1 / (1 - 3 ^ (-(3 * (1 - γ) / 4))); have ell := fun (j : ℤ) => if j ≤ k + ↑L then 1 else L; have p := fun (r : ℤ) => meanPenalty Q (relMean P q r (n + 2 * ↑L)); have decay := fun (j : ℤ) => 3 ^ (-(1 - γ) * (↑j - ↑jStar)); have M := fun (j : ℤ) => if j < ↑jStar + ↑L then Ce * B ^ Q else Cm * (p (j - ↑(ell j)) + ∑ r ∈ Finset.Icc (↑jStar) (j - ↑(ell j) - 1), 3 ^ (-(1 - γ) * (↑j - ↑r)) * p r + δ + B ^ Q * (decay j + decay j ^ Q)); (∀ j ∈ Finset.Icc (↑jStar) (n + ↑L), 0 ≤ M j) ∧ ∑ j ∈ Finset.Icc (↑jStar) (n + ↑L), 3 ^ (-a * (↑n + ↑L - ↑j)) * M j ≤ Cm * ((2 + G₃) * (2 + G₁) * 3 ^ ((1 - γ) / 2 * ↑L) * profile P γ q jStar k (n + 2 * ↑L) + G₁ * δ + 2 * G₃ * B ^ Q * 3 ^ (-a * (↑n - ↑jStar))) + Ce * G₁ * B ^ Q * 3 ^ (-a * (↑n - ↑jStar))

Accumulation of the actual bulk and boundary means, comparison error and both source powers, with the early target range kept separate.

theorem HCPolySupport.HighContrast.Annealed.transport_target_source_moments {d Q : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hQ : 1 ≤ Q) (F : CoeffSpace d → BlockMat d) (hF : SchattenMemLp P (↑Q) F) (hF0 : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (ofFullBlockMat 0) (F a)) (X : CoeffSpace d → ℝ) (hX : MeasureTheory.Integrable X P) (hEX : ∫ (a : CoeffSpace d), X a ∂P ≤ 2) (C B : ℝ) (hC : 0 ≤ C) (hB : 1 ≤ B) (hbound : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (F a) (blockScale (C * B * X a) (Book.Ch02.blockIdentity d))) : have MF := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (F a) α β ∂P); BlockMatLoewnerLE (Book.Ch02.blockIdentity d) MF → (∀ᵐ (a : CoeffSpace d) ∂P, absSchattenNorm (↑Q) (blockSub (F a) MF) ≤ 2 * ↑d * C * B * (X a + 2)) ∧ meanPenalty Q MF ≤ (1 + 4 * ↑d * C) ^ Q * B ^ Q

The source bound on an actual target controls both its centered matrix and its deterministic mean penalty with the same geometric amplitude.

theorem HCPolySupport.HighContrast.Annealed.exists_two_grid_profile_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 → 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 → 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))) → profile P γ (Geometry.explicitRoundedGrid jStar mPlus) jStar (n + ↑L) (n + ↑L) ≤ C * 3 ^ ((1 - γ) / 2 * ↑L) * profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k (n + 2 * ↑L) + C * δ + C * (1 + aspectRatio E * (K₀ * √(‖m‖ * ‖m⁻¹‖) * √(‖mPlus‖ * ‖mPlus⁻¹‖) + √(‖mPlus‖ * ‖mPlus⁻¹‖) ^ 2)) ^ bigQ d γ * 3 ^ (-((1 - γ) / 4) * (↑n - ↑jStar))

The complete printed profile comparison. All constants precede the law, geometry and comparison error; both source amplitudes retain their asymmetry.