High-contrast homogenization: Entry.Annealed.TransportProfile #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Boundary profiles for the two-grid transport #
The old-history boundary and bulk profile bounds behind p.two.grid.transport. All
generations at or below the cutoff k are dominated by one common parent-history envelope
under a single target maximum, and the actual Whitney rows are exhibited with their
mass-one identity and weighted row bounds, so the complete boundary fluctuation history is
paid by the fine profile. The above-k bulk rows are then reindexed through the target
cardinalities and the two generation values and are again absorbed by the profile.
Supporting this, block subtraction is subtraction of full matrices, normalization commutes
with it, and the transported trace loses no dimensional factor; the mean-penalty split is
carried to the actual old-grid means through three ordered normalizers, and the exact
mean-weight ratio yields the printed half-(1 - γ) loss in L for the initial, later and
bulk mean rows.
theorem
HCPolySupport.HighContrast.Annealed.transport_old_boundary_profile
(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)
(qPlus : Mat d)
(k n : ℤ)
(hk : ↑jStar ≤ k)
(hkn : k ≤ n)
(L h : ℕ)
(hcover : adaptedCell qPlus (n + ↑L) ⊆ adaptedCell (Geometry.explicitRoundedGrid jStar m) (n + ↑L + ↑h))
{ι : Type u_1}
(I : Finset ι)
(hI : I.Nonempty)
(j cap : ι → ℤ)
(D : ℝ)
(hD : 0 ≤ D)
(Z : ι → ℤ → Finset (Vec d))
(v : ι → ℤ → ℝ)
(hcapk : ∀ i ∈ I, cap i ≤ k)
(hcapj : ∀ i ∈ I, cap i ≤ j i)
(hZ :
∀ i ∈ I,
∀ r ∈ Finset.Icc (↑jStar) (cap i),
↑(Z i r) ⊆ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar m) r ∩ adaptedCell qPlus (n + ↑L))
(hv : ∀ i ∈ I, ∀ r ∈ Finset.Icc (↑jStar) (cap i), 0 ≤ v i r)
(hmass : ∀ i ∈ I, ∀ r ∈ Finset.Icc (↑jStar) (cap i), ∑ _z ∈ Z i r, v i r ≤ D * 3 ^ (↑r - ↑(j i)))
:
have q := Geometry.explicitRoundedGrid jStar m;
have Q := bigQ d γ;
have Cb := D * (1 / (1 - 3 ^ (-(1 - rhoMax d γ))));
∫ (a : CoeffSpace d), (⨆ i ∈ ↑I,
3 ^ (-rhoMax d γ * (↑n + ↑L - ↑(j i))) * ∑ r ∈ Finset.Icc (↑jStar) (cap i),
absSchattenNorm (↑Q)
(ofFullBlockMat (∑ z ∈ Z i r, v i r • toFullBlockMat (normalizedFluctuation P q r (n + 2 * ↑L) z a)))) ^ ↑Q ∂P ≤ Cb ^ Q * (2 * ↑d * 3 ^ (↑Q * rhoMax d γ + ↑d * ↑h)) * 3 ^ ((1 - γ) / 4 * ↑L) * profile P γ q jStar k (n + 2 * ↑L)
The boundary generations at or below k use one common parent-history field under the complete target maximum.
theorem
HCPolySupport.HighContrast.Annealed.exists_transport_whitney_rows
(d : ℕ)
(hd : 2 ≤ d)
(K₀ : ℝ)
(hK₀ : 1 ≤ K₀)
(γ : ℝ)
(hγ : γ ∈ Set.Ico 0 1)
:
∃ (Csrc : ℝ),
0 < Csrc ∧ ∃ (C : ℝ),
0 < C ∧ ∀ (K : ℝ),
1 < K →
∀ (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 t : ℤ) (L : ℕ),
1 ≤ L →
let q := Geometry.explicitRoundedGrid jStar m;
let qPlus := Geometry.explicitRoundedGrid jStar mPlus;
let ell := fun (j : ℤ) => if j ≤ k + ↑L then 1 else L;
let cap := fun (j : ℤ) => j - ↑(ell j);
let W := fun (p : ℤ × (Fin d → ℤ)) => adaptedCellAtCenter qPlus p.1 p.2;
∀ (I : Finset (ℤ × (Fin d → ℤ))),
(∀ p ∈ I, p.1 ≤ t) →
(∀ p ∈ I, standardCellCenter p.1 p.2 ∈ centeredCube d t) →
∃ (hfin :
∀ (p : ℤ × (Fin d → ℤ)),
∀ r ≤ cap p.1, (maximalAdaptedCellCenters (W p) q (cap p.1) r).Finite),
have Z := fun (p : ℤ × (Fin d → ℤ)) (r : ℤ) =>
if hr : r ≤ cap p.1 then ⋯.toFinset else ∅;
have v := fun (p : ℤ × (Fin d → ℤ)) (r : ℤ) =>
(MeasureTheory.volume (adaptedCell q r)).toReal / (MeasureTheory.volume (W p)).toReal;
∀ p ∈ I,
(∀ r ≤ cap p.1, ↑(Z p r) ⊆ adaptedLatticeAtScale q r ∩ adaptedCell qPlus t) ∧ ∑ _z ∈ Z p (cap p.1), v p (cap p.1) ≤ 1 ∧ (∑ _z ∈ Z p (cap p.1), v p (cap p.1) ^ 2) ^ (1 / 2) ≤ C * 3 ^ (-↑d / 2 * ↑(ell p.1)) ∧ ∀ r < cap p.1,
(∑ _z ∈ Z p r, v p r ^ 2) ^ (1 / 2) ≤ C * 3 ^ (-(↑d + 1) / 2 * (↑p.1 - ↑r)) ∧ ∑ _z ∈ Z p r, v p r ≤ C * 3 ^ (↑r - ↑p.1)
The actual Whitney rows supply all row guards simultaneously. The mass-one identity also pays the cap row, including an empty row.
theorem
HCPolySupport.HighContrast.Annealed.exists_transport_boundary_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 → ℤ)) (r : ℤ) =>
if hr : r ≤ cap p.1 then ⋯.toFinset else ∅;
have v := fun (p : ℤ × (Fin d → ℤ)) (r : ℤ) =>
(MeasureTheory.volume (adaptedCell q r)).toReal / (MeasureTheory.volume (W p)).toReal;
∫ (a : CoeffSpace d), (⨆ p ∈ ↑I,
3 ^ (-rhoMax d γ * (↑n + ↑L - ↑p.1)) * ∑ r ∈ Finset.Icc (↑jStar) (cap p.1 - 1),
absSchattenNorm (↑Q)
(ofFullBlockMat
(∑ z ∈ Z p r,
v p r • toFullBlockMat
(normalizedFluctuation P q r (n + 2 * ↑L) z
a)))) ^ ↑Q ∂P ≤ C * 3 ^ ((1 - γ) / 4 * ↑L) * profile P γ q jStar k (n + 2 * ↑L)
The printed boundary fluctuation estimate for the actual Whitney rows, with the old and averaged generations combined under one joint maximum.
theorem
HCPolySupport.HighContrast.Annealed.exists_transport_high_bulk_profile
(d : ℕ)
(hd : 2 ≤ d)
(γ : ℝ)
(hγ : γ ∈ Set.Ico 0 1)
:
∃ (Csrc : ℝ),
0 < Csrc ∧ ∀ (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 : Mat d),
Matrix.PosDef m →
∀ (k n : ℤ),
↑jStar ≤ k →
k ≤ n →
∀ (L : ℕ) (D : ℝ),
0 ≤ D →
have q := Geometry.explicitRoundedGrid jStar m;
have Q := bigQ d γ;
have ell := fun (j : ℤ) => if j ≤ k + ↑L then 1 else L;
have r := fun (j : ℤ) => j - ↑(ell j);
∀ (I : Finset (ℤ × (Fin d → ℤ))),
I.Nonempty →
∀ (Z : ℤ × (Fin d → ℤ) → Finset (Vec d)) (v : ℤ × (Fin d → ℤ) → ℝ),
(∀ i ∈ I, r i.1 ∈ Finset.Icc (k + 1) (n + 2 * ↑L)) →
(∀ i ∈ I, i.1 ≤ n + ↑L) →
(∀ j ∈ Finset.image Prod.fst I,
↑{i ∈ I | i.1 = j}.card ≤ 3 ^ (↑d * (↑n + ↑L - ↑j))) →
(∀ i ∈ I, ↑(Z i) ⊆ adaptedLatticeAtScale q (r i.1)) →
(∀ i ∈ I, 0 ≤ v i) →
(∀ i ∈ I,
(∑ _z ∈ Z i, v i ^ 2) ^ (1 / 2) ≤ D * 3 ^ (-↑d / 2 * ↑(ell i.1))) →
∫ (a : CoeffSpace d), (⨆ i ∈ ↑I,
3 ^ (-rhoMax d γ * (↑n + ↑L - ↑i.1)) * absSchattenNorm (↑Q)
(ofFullBlockMat
(∑ z ∈ Z i,
v i • toFullBlockMat
(normalizedFluctuation P q (r i.1) (n + 2 * ↑L)
z a)))) ^ ↑Q ∂P ≤ 2 * (↑Q * 3 ^ (↑d / 2) * D) ^ Q * 3 ^ ((1 - γ) / 4 * ↑L) * profile P γ q jStar k (n + 2 * ↑L)
The above-k bulk rows are paid by the last sum in the actual profile. Target cardinalities enter before the two-value generation reindexing.
theorem
HCPolySupport.HighContrast.Annealed.transport_normalized_trace_le
{d : ℕ}
{X R S : BlockMat d}
(hX : Matrix.PosSemidef (toFullBlockMat X))
(hR : Matrix.PosDef (toFullBlockMat R))
(hS : Matrix.PosDef (toFullBlockMat S))
:
blockTrace (normalizedBlock X S) ≤ blockOpNorm (normalizedBlock R S) * blockTrace (normalizedBlock X R)
Trace transport for a positive matrix, with no dimensional loss.
theorem
HCPolySupport.HighContrast.Annealed.transport_meanPenalty_split
{d : ℕ}
(Q : ℕ)
(A B C : BlockMat d)
(hA : Matrix.PosDef (toFullBlockMat A))
(hB : Matrix.PosDef (toFullBlockMat B))
(hC : Matrix.PosDef (toFullBlockMat C))
(hBA : BlockMatLoewnerLE B A)
(hCB : BlockMatLoewnerLE C B)
:
meanPenalty Q (normalizedBlock A C) ≤ (1 + meanPenalty Q (normalizedBlock B C)) * meanPenalty Q (normalizedBlock A B) + meanPenalty Q (normalizedBlock B C)
The printed mean-penalty split for three ordered positive normalizers.
theorem
HCPolySupport.HighContrast.Annealed.transport_meanPenalty_split_scales
(d : ℕ)
(hd : 2 ≤ d)
(P : MeasureTheory.Measure (CoeffSpace d))
[MeasureTheory.IsProbabilityMeasure P]
(γ : ℝ)
(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)
(r k t : ℤ)
(hr : ↑jStar ≤ r)
(hrk : r ≤ k)
(hkt : k ≤ t)
:
have q := Geometry.explicitRoundedGrid jStar m;
meanPenalty (bigQ d γ) (relMean P q r t) ≤ (1 + meanPenalty (bigQ d γ) (relMean P q k t)) * meanPenalty (bigQ d γ) (relMean P q r k) + meanPenalty (bigQ d γ) (relMean P q k t)
The same split at the actual old-grid means; all order and positivity hypotheses come from the standing law and the generation order.
theorem
HCPolySupport.HighContrast.Annealed.transport_initial_mean_history
(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 t : ℤ)
(hk : ↑jStar ≤ k)
(hkt : k ≤ t)
:
The initial mean history is part of the first profile summand.
theorem
HCPolySupport.HighContrast.Annealed.transport_later_mean_row
(d : ℕ)
(hd : 2 ≤ d)
(P : MeasureTheory.Measure (CoeffSpace d))
[MeasureTheory.IsProbabilityMeasure P]
(γ : ℝ)
(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 t : ℤ)
(hk : ↑jStar ≤ k)
(r : ℤ)
(hr : r ∈ Finset.Ico k t)
:
have q := Geometry.explicitRoundedGrid jStar m;
3 ^ (-((1 - γ) / 4) * (↑t - 1 - ↑r)) * meanPenalty (bigQ d γ) (relMean P q r t) ≤ meanHistory P γ q k t
A later mean row belongs to the Ico range, which excludes the terminal scale.
theorem
HCPolySupport.HighContrast.Annealed.transport_meanHistory_to_profile
(d : ℕ)
(hd : 2 ≤ d)
(P : MeasureTheory.Measure (CoeffSpace d))
[MeasureTheory.IsProbabilityMeasure P]
(γ : ℝ)
(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 t : ℤ)
(hk : ↑jStar ≤ k)
(hkt : k < t)
:
Changing the starting scale of the full mean history is paid by the initial and later profile components, with an explicit geometric constant.
theorem
HCPolySupport.HighContrast.Annealed.transport_bulk_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)) * meanPenalty (bigQ d γ) (relMean P q (j - ↑(ell j)) (n + 2 * ↑L)) ≤ 2 * (2 + 1 / (1 - 3 ^ (-((1 - γ) / 4)))) * 3 ^ ((1 - γ) / 2 * ↑L) * profile P γ q jStar k (n + 2 * ↑L)
The actual bulk mean sum has the printed half-(1-gamma) loss in L.