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

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

Initialization: Step 2, the logarithmic decrement and its budget

Step 2 of the printed proof (p.initial.fixed.grid.scale): along the synchronized scales T_ℓ = R + 2Q + ℓ·2Q the logarithm W_ℓ = log(1 + η₀⁻¹(𝒫_Id(T_ℓ;j_*) + D_{Id,j_*}(T_ℓ))) drops by log(16/9) per step up to a determinant-loss defect, the accumulated synchronized losses are bounded by C log₃(2 + Π), and the starting value is bounded by C(d,γ,η₀) log₃(2 + Π).

theorem HCPolySupport.HighContrast.Multiscale.initial_log_decrement (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ η₀ ∈ Set.Ioc 0 1, ∃ (C : ℝ), 0 < C ∧ ∀ (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 → ∀ (R : ℤ), ↑jStar ≤ R → ∀ (ℓ : ℕ), η₀ < profile P γ 1 jStar (↑jStar) (R + 2 * ↑(bigQ d γ) + ↑ℓ * (2 * ↑(bigQ d γ))) + determinantDrift P γ 1 jStar (R + 2 * ↑(bigQ d γ) + ↑ℓ * (2 * ↑(bigQ d γ))) → Real.log (1 + η₀⁻¹ * (profile P γ 1 jStar (↑jStar) (R + 2 * ↑(bigQ d γ) + ↑(ℓ + 1) * (2 * ↑(bigQ d γ))) + determinantDrift P γ 1 jStar (R + 2 * ↑(bigQ d γ) + ↑(ℓ + 1) * (2 * ↑(bigQ d γ))))) ≤ Real.log (1 + η₀⁻¹ * (profile P γ 1 jStar (↑jStar) (R + 2 * ↑(bigQ d γ) + ↑ℓ * (2 * ↑(bigQ d γ))) + determinantDrift P γ 1 jStar (R + 2 * ↑(bigQ d γ) + ↑ℓ * (2 * ↑(bigQ d γ))))) - Real.log (16 / 9) + C * synchCharge P 1 (2 * ↑(bigQ d γ)) (R + 2 * ↑(bigQ d γ) + ↑ℓ * (2 * ↑(bigQ d γ)))

E4. e.initial.log.decrement (p.initial.fixed.grid.scale) at the synchronized scales T_ℓ = R + 2Q + ℓ·2Q, with W_ℓ = log(1 + η₀⁻¹(𝒫_Id(T_ℓ;j_*) + D_{Id,j_*}(T_ℓ))).

theorem HCPolySupport.HighContrast.Multiscale.synchronized_loss_budget_one (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (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 → ∀ (R : ℤ), ↑jStar ≤ R → ∀ (Ksteps : ℕ), 1 ≤ Ksteps → ∑ ℓ ∈ Finset.range Ksteps, synchCharge P 1 (2 * ↑(bigQ d γ)) (R + 2 * ↑(bigQ d γ) + ↑ℓ * (2 * ↑(bigQ d γ))) ≤ C * Real.logb 3 (2 + aspectRatio E)

E5. The synchronized determinant budget (p.initial.fixed.grid.scale): ∑_{ℓ<K} Δ̂_h(T_ℓ) ≤ h Δ_{T_0+1−h, T_0+Kh} ≤ C log₃(2+Π).

theorem HCPolySupport.HighContrast.Multiscale.starting_log_le_one (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ η₀ ∈ Set.Ioc 0 1, ∃ (C : ℝ), 0 < C ∧ ∀ (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 → Real.log (1 + η₀⁻¹ * (profile P γ 1 jStar (↑jStar) m + determinantDrift P γ 1 jStar m)) ≤ C * Real.logb 3 (2 + aspectRatio E)

E6. e.initial.starting.log: W ≤ C(d,γ,η₀) log₃(2+Π) at every m ≥ j_*.