High-contrast homogenization: Entry.Multiscale.ScaleSelection.Alternatives

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

The startup, service and obstruction alternatives

Group D of the printed proof (p.scale.selection), first part: alternative 1 in its start-up case k = n and its service case k < n, and the two determinant-obstruction clauses of alternative 3, each stated at the literal selection data so that its conclusion is the corresponding clause of SelectionData.Selects.

Part of the proof of the statement in HCPoly/Entry/Statements/ScaleSelection.lean. Conventions of the group: q = 𝒬(𝔪) is Geometry.explicitRoundedGrid jStar m; the printed data are h = 2Q, c = c₀, L(ε,σ) = selectionLength L₀ σ and B₀(ε,σ) = max 1 (max (B₀^bridge (√ε σ) L) (2 C_tr (L+1))); √ε is the printed ε^{1/2}; the source lower scale e.source.lower.scale is carried wherever j_* appears with the law, and no integrability, finiteness or measurability premise is added anywhere. Unused hypothesis binders of a statement are underscore-prefixed; the tree compiles with -DwarningAsError=true.

The declaration text of this file is the closed skeleton's, copied unchanged; only this header, the imports and the namespace frame are new.

Group D — the five alternatives (p.scale.selection)

Every alternative lemma is stated at the concrete data h = 2Q, L = selectionLength L₀ σ, η = c₀ ε σ, with the target constant C bounded below explicitly, so that its conclusion is literally the corresponding clause of SelectionData.Selects.

theorem HCPolySupport.HighContrast.Multiscale.startup_alternative (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (Csrc C₁ : ℝ) (hC₁ : 0 < C₁) (hone : OneGridBody d γ Csrc C₁) (C : ℝ) (hC : 2 * ↑(bigQ d γ) * C₁ ≤ C) (L₀ : ℕ) (ε σ B : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hP : MeasureTheory.IsProbabilityMeasure P) (hstat : IsStationaryLaw P) (hunit : IsUnitRangeLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (hsrc : ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar) (m : Mat d) (hm : Matrix.PosDef m) (k n : ℤ) (hjk : ↑jStar ≤ k) (hkn : k ≤ n) (hecc : 1 / 2 * Real.log (‖m‖ * ‖m⁻¹‖) ≤ ε / ↑(selectionLength L₀ σ) * (↑k - ↑jStar - ↑⌈B * Real.logb 3 (2 + aspectRatio E)⌉)) (hin1 : k = n → profile P γ (Geometry.explicitRoundedGrid jStar m) jStar n n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n ≤ 1) (hk : k = n) : (k = n ∧ profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k (n + ↑(2 * bigQ d γ)) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + ↑(2 * bigQ d γ)) ≤ C * (profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n + Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar m) n (n + ↑(2 * bigQ d γ))) - 1)) ∧ 1 / 2 * Real.log (‖m‖ * ‖m⁻¹‖) ≤ ε / ↑(selectionLength L₀ σ) * (↑k - ↑jStar - ↑⌈B * Real.logb 3 (2 + aspectRatio E)⌉) ∧ (k = n + ↑(2 * bigQ d γ) → profile P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + ↑(2 * bigQ d γ)) (n + ↑(2 * bigQ d γ)) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + ↑(2 * bigQ d γ)) ≤ 1) ∧ (k < n + ↑(2 * bigQ d γ) → k + ↑(2 * bigQ d γ) ≤ n + ↑(2 * bigQ d γ))

Alternative 1, k = n (p.scale.selection): startup from the one-grid fixed-span propagation at span h = 2Q, together with the two output conditions of Step 3.

theorem HCPolySupport.HighContrast.Multiscale.service_alternative (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (Csrc C₁ : ℝ) (hC₁ : 0 < C₁) (hone : OneGridBody d γ Csrc C₁) (C : ℝ) (hC : 2 * ↑(bigQ d γ) * C₁ ≤ C) (L₀ : ℕ) (c₀ ε σ B : ℝ) (hσ : σ ∈ Set.Ioc 0 ε) (hQε : ↑(bigQ d γ) * ↑d * ε ≤ Real.log 2) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hP : MeasureTheory.IsProbabilityMeasure P) (hstat : IsStationaryLaw P) (hunit : IsUnitRangeLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (hsrc : ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar) (m : Mat d) (hm : Matrix.PosDef m) (k n : ℤ) (hjk : ↑jStar ≤ k) (hkn : k ≤ n) (hecc : 1 / 2 * Real.log (‖m‖ * ‖m⁻¹‖) ≤ ε / ↑(selectionLength L₀ σ) * (↑k - ↑jStar - ↑⌈B * Real.logb 3 (2 + aspectRatio E)⌉)) (hin2 : k < n → k + ↑(2 * bigQ d γ) ≤ n) (hk : k < n) (hη : profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n > c₀ * ε * σ) (hsync : (↑d)⁻¹ * synchCharge P (Geometry.explicitRoundedGrid jStar m) (↑(2 * bigQ d γ)) n ≤ σ) : (k < n ∧ profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n > c₀ * ε * σ ∧ (↑d)⁻¹ * synchCharge P (Geometry.explicitRoundedGrid jStar m) (↑(2 * bigQ d γ)) n ≤ σ ∧ profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k (n + ↑(2 * bigQ d γ)) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + ↑(2 * bigQ d γ)) ≤ 1 / 4 * (profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n) + C * synchCharge P (Geometry.explicitRoundedGrid jStar m) (↑(2 * bigQ d γ)) n) ∧ 1 / 2 * Real.log (‖m‖ * ‖m⁻¹‖) ≤ ε / ↑(selectionLength L₀ σ) * (↑k - ↑jStar - ↑⌈B * Real.logb 3 (2 + aspectRatio E)⌉) ∧ (k = n + ↑(2 * bigQ d γ) → profile P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + ↑(2 * bigQ d γ)) (n + ↑(2 * bigQ d γ)) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + ↑(2 * bigQ d γ)) ≤ 1) ∧ (k < n + ↑(2 * bigQ d γ) → k + ↑(2 * bigQ d γ) ≤ n + ↑(2 * bigQ d γ))

Alternative 1, k < n, synchronized test passed (p.scale.selection): service from the one-grid synchronized propagation, Q Δ̂ ≤ Qdσ ≤ Qdε₀ ≤ log 2, and Step 3.

theorem HCPolySupport.HighContrast.Multiscale.obstruction_sync_alternative (d : ℕ) (γ : ℝ) (L₀ : ℕ) (c₀ ε σ B : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (jStar : ℕ) (m : Mat d) (k n : ℤ) (hecc : 1 / 2 * Real.log (‖m‖ * ‖m⁻¹‖) ≤ ε / ↑(selectionLength L₀ σ) * (↑k - ↑jStar - ↑⌈B * Real.logb 3 (2 + aspectRatio E)⌉)) (hk : k < n) (hη : profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n > c₀ * ε * σ) (hsync : (↑d)⁻¹ * synchCharge P (Geometry.explicitRoundedGrid jStar m) (↑(2 * bigQ d γ)) n > σ) : (k < n ∧ profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n > c₀ * ε * σ ∧ (↑d)⁻¹ * synchCharge P (Geometry.explicitRoundedGrid jStar m) (↑(2 * bigQ d γ)) n > σ) ∧ 1 / 2 * Real.log (‖m‖ * ‖m⁻¹‖) ≤ ε / ↑(selectionLength L₀ σ) * (↑k - ↑jStar - ↑⌈B * Real.logb 3 (2 + aspectRatio E)⌉) ∧ (k = n + ↑(2 * bigQ d γ) → profile P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + ↑(2 * bigQ d γ)) (n + ↑(2 * bigQ d γ)) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + ↑(2 * bigQ d γ)) ≤ 1) ∧ (k < n + ↑(2 * bigQ d γ) → k + ↑(2 * bigQ d γ) ≤ n + ↑(2 * bigQ d γ))

Alternative 3, synchronized obstruction (p.scale.selection): pure bookkeeping.

theorem HCPolySupport.HighContrast.Multiscale.obstruction_long_alternative (d : ℕ) (γ : ℝ) (L₀ : ℕ) (c₀ ε σ B : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (jStar : ℕ) (m : Mat d) (k n : ℤ) (hecc : 1 / 2 * Real.log (‖m‖ * ‖m⁻¹‖) ≤ ε / ↑(selectionLength L₀ σ) * (↑k - ↑jStar - ↑⌈B * Real.logb 3 (2 + aspectRatio E)⌉)) (hin2 : k < n → k + ↑(2 * bigQ d γ) ≤ n) (hk : k < n) (hη : profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n ≤ c₀ * ε * σ) (hlong : (↑d)⁻¹ * detIncrement P (Geometry.explicitRoundedGrid jStar m) n (n + 2 * ↑(selectionLength L₀ σ)) > ε * σ) : (k < n ∧ profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n ≤ c₀ * ε * σ ∧ (↑d)⁻¹ * detIncrement P (Geometry.explicitRoundedGrid jStar m) n (n + 2 * ↑(selectionLength L₀ σ)) > ε * σ) ∧ 1 / 2 * Real.log (‖m‖ * ‖m⁻¹‖) ≤ ε / ↑(selectionLength L₀ σ) * (↑k - ↑jStar - ↑⌈B * Real.logb 3 (2 + aspectRatio E)⌉) ∧ (k = n + 2 * ↑(selectionLength L₀ σ) → profile P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + 2 * ↑(selectionLength L₀ σ)) (n + 2 * ↑(selectionLength L₀ σ)) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + 2 * ↑(selectionLength L₀ σ)) ≤ 1) ∧ (k < n + 2 * ↑(selectionLength L₀ σ) → k + ↑(2 * bigQ d γ) ≤ n + 2 * ↑(selectionLength L₀ σ))

Alternative 3, long obstruction (p.scale.selection): pure bookkeeping.