High-contrast homogenization: Entry.Multiscale.Initial.CrudeProfile

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

Initialization: Step 1, the crude profile bound

Step 1 of the printed proof (p.initial.fixed.grid.scale): at the Euclidean grid and the seed generation j_* the mean history, the determinant drift and the profile are each bounded by C (2 + Π)^N with C and N depending only on d and γ. The seed bound needs only the single-cell fluctuation history at j_*, not the fluctuation history at a general generation.

D. Step 1 — the crude profile bound (p.initial.fixed.grid.scale)

theorem HCPolySupport.HighContrast.Multiscale.meanHistory_one_le (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (n m : ℤ), ↑jStar ≤ n → n ≤ m → meanHistory P γ 1 n m ≤ ((1 + 2 * ↑d * (24 * aspectRatio E - 1)) ^ bigQ d γ - 1) * (1 - 3 ^ (-((1 - γ) / 4)))⁻¹

D1. ℋ^mean_Id(m;n) ≤ C(2+Π)^C (p.initial.fixed.grid.scale).

theorem HCPolySupport.HighContrast.Multiscale.determinantDrift_one_le (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m : ℤ), ↑jStar ≤ m → determinantDrift P γ 1 jStar m ≤ 2 * ↑d * (24 * aspectRatio E - 1)

D2. D_{Id,j_*}(m) ≤ tr(P^Id_{j_*,m} − I) ≤ CΠ (p.initial.fixed.grid.scale).

theorem HCPolySupport.HighContrast.Multiscale.profile_one_seed_le (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m : ℤ), ↑jStar ≤ m → 3 ^ (-((1 - γ) / 4) * (↑m - ↑↑jStar)) * (1 + meanPenalty (bigQ d γ) (relMean P 1 (↑jStar) m)) * history P γ 1 jStar ↑jStar ≤ (1 + 2 * ↑d * (24 * aspectRatio E - 1)) ^ bigQ d γ * (2 * ↑d * (1 + (24 * aspectRatio E) ^ bigQ d γ))

D3. The seed term of 𝒫_Id(m;j_*) (p.initial.fixed.grid.scale).

theorem HCPolySupport.HighContrast.Multiscale.profile_one_fluct_sum_le (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m : ℤ), ↑jStar ≤ m → ∑ j ∈ Finset.Icc (↑jStar + 1) m, 3 ^ (-((1 - γ) / 4) * (↑m - ↑j)) * Real.exp (↑(bigQ d γ) * detIncrement P 1 j m) * ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d γ)) (normalizedFluctuationSelf P 1 j a) ^ bigQ d γ ∂P ≤ (24 * aspectRatio E) ^ (2 * d * bigQ d γ) * (2 * ↑d * (1 + (24 * aspectRatio E) ^ bigQ d γ)) * (1 - 3 ^ (-((1 - γ) / 4)))⁻¹

D4. The new-fluctuation sum of 𝒫_Id(m;j_*) (p.initial.fixed.grid.scale).

theorem HCPolySupport.HighContrast.Multiscale.initial_crude_profile (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m : ℤ), ↑jStar ≤ m → profile P γ 1 jStar (↑jStar) m + determinantDrift P γ 1 jStar m ≤ C * (2 + aspectRatio E) ^ N

D5. e.initial.crude.profile: 𝒫_Id(m;j_*) + D_{Id,j_*}(m) ≤ C(2+Π)^N.