High-contrast homogenization: Provider.Quenched.SmallContrastFamilyLineClausesSrc #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The family recursion with the explicit source #
The line chain of SmallContrastSharpLineAtJb through
SmallContrastFamilyLineClausesSrc, with the entry pricing clause removed:
the per-generation recursion carries the entry-slot source term
3·wC·(weakSourceGroupSummed …)² explicitly, so the corrected
three-channel pricing can be applied to it downstream instead of the
geometric pre-pricing of the availability route.
theorem
HCPolySupport.HighContrast.Quenched.hrec_final_sharp_at_jb_src
{F : ℕ → ℝ}
(hFnn : ∀ (j : ℕ), 0 ≤ F j)
(hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p)
{r : ℝ}
(hr0 : 0 < r)
(hr1 : r < 1)
{n H jb : ℕ}
(hH : H + 1 ≤ n)
(hjbn : jb ≤ n)
{a bq cw : ℝ}
(ha : 0 ≤ a)
(hbq0 : 0 ≤ bq)
(hcw : 0 ≤ cw)
{W u v w cdrop : ℝ}
(hW0 : 0 ≤ W)
(hstep : F n ≤ a * (F (n - H) - F n) + bq * F n ^ 2 + cw * W ^ 2)
(hWsplit : W ≤ u + v * F jb + w)
(hwsq : w ^ 2 ≤ cdrop * iterationDropSum r F n)
{A : ℝ}
(hA1 : a * (r ^ H)⁻¹ + 3 * cw * cdrop ≤ A)
(hA2 : bq + 3 * cw * v ^ 2 ≤ A)
:
hrec_final_sharp_at_jb_src with the source kept explicit.
theorem
HCPolySupport.HighContrast.Quenched.per_generation_hrec_at_recursionAlpha_sharp_at_jb_src
{F : ℕ → ℝ}
{g : ℝ}
(hg1 : g < 1)
(hFnn : ∀ (j : ℕ), 0 ≤ F j)
(hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p)
{n H jb : ℕ}
(hH : H + 1 ≤ n)
(hjbn : jb ≤ n)
{a bq cw : ℝ}
(ha : 0 ≤ a)
(hbq0 : 0 ≤ bq)
(hcw : 0 ≤ cw)
{W u v w cdrop : ℝ}
(hW0 : 0 ≤ W)
(hstep : F n ≤ a * (F (n - H) - F n) + bq * F n ^ 2 + cw * W ^ 2)
(hWsplit : W ≤ u + v * F jb + w)
(hwsq : w ^ 2 ≤ cdrop * iterationDropSum (3 ^ (-recursionAlpha g)) F n)
{A : ℝ}
(hA1 : a * ((3 ^ (-recursionAlpha g)) ^ H)⁻¹ + 3 * cw * cdrop ≤ A)
(hA2 : bq + 3 * cw * v ^ 2 ≤ A)
:
per_generation_hrec_at_recursionAlpha_sharp_at_jb_src with the source
kept explicit.
theorem
HCPolySupport.HighContrast.Quenched.hrec_line_of_one_step_isotropy_sharp_at_jb_src
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{q : Mat d}
{N₀ n H jb : ℕ}
(hH : H + 1 ≤ n)
(hjbn : jb ≤ n)
(hFnn : ∀ (j : ℕ), 0 ≤ hatExcess P q N₀ j)
(hFmono : ∀ (p j : ℕ), p ≤ j → hatExcess P q N₀ j ≤ hatExcess P q N₀ p)
{g : ℝ}
(hg1 : g < 1)
{Cpre eta cRow kap : ℝ}
(hCpre : 0 ≤ Cpre)
(heta : 0 < eta)
{wv W u v w cdrop A : ℝ}
(hW0 : 0 ≤ W)
(hmaj : wv ≤ W ^ 2)
(hquad0 : 0 ≤ quadCoefficient d Cpre (rowCoefficientIsotropy d cRow kap))
(hone :
adaptedHattedContrast P q (↑N₀ + ↑n) - 1 ≤ 4 * Cpre * ((3 / 2 + 1 / (4 * eta)) * (16 * ↑d * (adaptedHattedContrast P q (↑N₀ + ↑(n - H)) - adaptedHattedContrast P q (↑N₀ + ↑n))) + rowValue2Isotropy d cRow kap (↑d * (adaptedHattedContrast P q (↑N₀ + ↑n) - 1)) + wv) + 2 * ((3 * ↑d + 4) * (↑d * (adaptedHattedContrast P q (↑N₀ + ↑n) - 1)) ^ 2))
(hWsplit : W ≤ u + v * hatExcess P q N₀ jb + w)
(hwsq : w ^ 2 ≤ cdrop * iterationDropSum (3 ^ (-recursionAlpha g)) (hatExcess P q N₀) n)
(hA1 : dropCoefficient d Cpre eta * ((3 ^ (-recursionAlpha g)) ^ H)⁻¹ + 3 * weakCoefficient d Cpre * cdrop ≤ A)
(hA2 : quadCoefficient d Cpre (rowCoefficientIsotropy d cRow kap) + 3 * weakCoefficient d Cpre * v ^ 2 ≤ A)
:
hrec_line_of_one_step_isotropy_sharp_at_jb_src with the source kept
explicit.
theorem
HCPolySupport.HighContrast.Quenched.hrec_line_of_slots_isotropy_sharp_at_jb_at_level_src
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{q : Mat d}
{N₀ n H Hw jb : ℕ}
(hH : H + 1 ≤ n)
(hHw : Hw + 1 ≤ n)
(hjbn : jb ≤ n)
(hFnn : ∀ (j : ℕ), 0 ≤ hatExcess P q N₀ j)
(hFmono : ∀ (p j : ℕ), p ≤ j → hatExcess P q N₀ j ≤ hatExcess P q N₀ p)
{g : ℝ}
(hg0 : 0 ≤ g)
(hg1 : g < 1)
{Cpre eta cRow kap : ℝ}
(hCpre : 0 ≤ Cpre)
(heta : 0 < eta)
(hcRow : 0 ≤ cRow)
(hkap : 0 ≤ kap)
{M L : ℝ}
(hM0 : 0 ≤ M)
{V : ℕ → ℝ}
{V0 : ℝ}
{Dr : ℕ → ℝ}
{Vmean bmaj beta lev : ℝ}
(hV : ∀ (j : ℕ), 0 ≤ V j)
(hV0 : 0 ≤ V0)
(hDrnn : ∀ (j : ℕ), 0 ≤ Dr j)
(hVmean0 : 0 ≤ Vmean)
(hbmaj : 0 ≤ bmaj)
(hbeta : 0 ≤ beta)
{wv : ℝ}
(hmaj : wv ≤ weakValueBaseIsotropyAtPar 16 16 M L (contrastRho g) Hw bmaj beta lev V V0 Dr Vmean ^ 2)
(hone :
adaptedHattedContrast P q (↑N₀ + ↑n) - 1 ≤ 4 * Cpre * ((3 / 2 + 1 / (4 * eta)) * (16 * ↑d * (adaptedHattedContrast P q (↑N₀ + ↑(n - H)) - adaptedHattedContrast P q (↑N₀ + ↑n))) + rowValue2Isotropy d cRow kap (↑d * (adaptedHattedContrast P q (↑N₀ + ↑n) - 1)) + wv) + 2 * ((3 * ↑d + 4) * (↑d * (adaptedHattedContrast P q (↑N₀ + ↑n) - 1)) ^ 2))
{vsum cVsum vmsrc cVm bsrc cD delta : ℝ}
(hcD0 : 0 ≤ cD)
(hdelta0 : 0 ≤ delta)
(hVsum : ∑ j ∈ Finset.range (Hw + 1), 3 ^ (-(1 / 2) * ↑j) * (V j + V0) ≤ vsum + cVsum * hatExcess P q N₀ jb)
(hVmeanle : Vmean ≤ vmsrc + cVm * hatExcess P q N₀ jb)
(hDrdelta : ∀ j ∈ Finset.range (Hw + 1), Dr j ≤ delta)
(hDrdrop : ∀ j ∈ Finset.range (Hw + 1), Dr j ≤ cD * (hatExcess P q N₀ (n - j) - hatExcess P q N₀ n))
(hbad :
√2 * √(L + 1) * Response.profileBadMajorantAt 4 bmaj beta lev + √2 * 3 ^ (-((1 - contrastRho g) / 2) * ↑Hw) * √(L + 1) ≤ bsrc)
:
hatExcess P q N₀ n ≤ fusionRecursionConstantIsotropySharp d Cpre eta H M L g cRow kap cD delta cVsum cVm * iterationDropSum (3 ^ (-recursionAlpha g)) (hatExcess P q N₀) n + fusionRecursionConstantIsotropySharp d Cpre eta H M L g cRow kap cD delta cVsum cVm * hatExcess P q N₀ jb ^ 2 + 3 * weakCoefficient d Cpre * weakSourceGroupSummed M L (contrastRho g) vsum vmsrc bsrc ^ 2
The released sharp slot line, with the source kept explicit.
theorem
HCPolySupport.HighContrast.Quenched.hline_of_slots_sharp_var_at_jb_at_level_src
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{q : Mat d}
{N₀ ns H : ℕ}
{Hw : ℕ → ℕ}
{g Cpre eta cRow kap M L cD delta : ℝ}
(hconst : IsotropySlotConstants d g Cpre eta cRow kap M cD delta)
(hFnn : ∀ (j : ℕ), 0 ≤ hatExcess P q N₀ j)
(hFmono : ∀ (p j : ℕ), p ≤ j → hatExcess P q N₀ j ≤ hatExcess P q N₀ p)
{V : ℕ → ℕ → ℝ}
{V0 : ℕ → ℝ}
{Dr : ℕ → ℕ → ℝ}
{Vmean bmaj : ℕ → ℝ}
{beta lev : ℝ}
{wv : ℕ → ℝ}
{jb : ℕ → ℕ}
{cVsum cVm : ℝ}
{vsum vmsrc bsrc : ℕ → ℝ}
(hV : ∀ (n j : ℕ), 0 ≤ V n j)
(hV0 : ∀ (n : ℕ), 0 ≤ V0 n)
(hDrnn : ∀ (n j : ℕ), 0 ≤ Dr n j)
(hVmean0 : ∀ (n : ℕ), 0 ≤ Vmean n)
(hbmaj : ∀ (n : ℕ), 0 ≤ bmaj n)
(hbeta : 0 ≤ beta)
(hbad :
∀ (n : ℕ),
√2 * √(L + 1) * Response.profileBadMajorantAt 4 (bmaj n) beta lev + √2 * 3 ^ (-((1 - contrastRho g) / 2) * ↑(Hw n)) * √(L + 1) ≤ bsrc n)
(hH : ∀ (n : ℕ), ns ≤ n → H + 1 ≤ n)
(hHw : ∀ (n : ℕ), ns ≤ n → Hw n + 1 ≤ n)
(hjbn : ∀ (n : ℕ), ns ≤ n → jb n ≤ n)
(hmaj :
∀ (n : ℕ),
ns ≤ n →
wv n ≤ weakValueBaseIsotropyAtPar 16 16 M L (contrastRho g) (Hw n) (bmaj n) beta lev (V n) (V0 n) (Dr n) (Vmean n) ^ 2)
(hone :
∀ (n : ℕ),
ns ≤ n →
adaptedHattedContrast P q (↑N₀ + ↑n) - 1 ≤ 4 * Cpre * ((3 / 2 + 1 / (4 * eta)) * (16 * ↑d * (adaptedHattedContrast P q (↑N₀ + ↑(n - H)) - adaptedHattedContrast P q (↑N₀ + ↑n))) + rowValue2Isotropy d cRow kap (↑d * (adaptedHattedContrast P q (↑N₀ + ↑n) - 1)) + wv n) + 2 * ((3 * ↑d + 4) * (↑d * (adaptedHattedContrast P q (↑N₀ + ↑n) - 1)) ^ 2))
(hVsum :
∀ (n : ℕ),
ns ≤ n →
∑ j ∈ Finset.range (Hw n + 1), 3 ^ (-(1 / 2) * ↑j) * (V n j + V0 n) ≤ vsum n + cVsum * hatExcess P q N₀ (jb n))
(hVmeanle : ∀ (n : ℕ), ns ≤ n → Vmean n ≤ vmsrc n + cVm * hatExcess P q N₀ (jb n))
(hDrdelta : ∀ (n : ℕ), ns ≤ n → ∀ j ∈ Finset.range (Hw n + 1), Dr n j ≤ delta)
(hDrdrop :
∀ (n : ℕ), ns ≤ n → ∀ j ∈ Finset.range (Hw n + 1), Dr n j ≤ cD * (hatExcess P q N₀ (n - j) - hatExcess P q N₀ n))
(n : ℕ)
:
ns ≤ n →
hatExcess P q N₀ n ≤ fusionRecursionConstantIsotropySharp d Cpre eta H M L g cRow kap cD delta cVsum cVm * iterationDropSum (3 ^ (-recursionAlpha g)) (hatExcess P q N₀) n + fusionRecursionConstantIsotropySharp d Cpre eta H M L g cRow kap cD delta cVsum cVm * hatExcess P q N₀ (jb n) ^ 2 + 3 * weakCoefficient d Cpre * weakSourceGroupSummed M L (contrastRho g) (vsum n) (vmsrc n) (bsrc n) ^ 2
The line producer with the source kept explicit.
theorem
HCPolySupport.HighContrast.Quenched.hline_of_slots_sharp_var_at_jb_of_at_level_clauses_src
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{q : Mat d}
{N₀ ns H : ℕ}
{Hw : ℕ → ℕ}
{g Cpre eta cRow kap M L cD delta cfirst cmax : ℝ}
(hcfirst : 0 ≤ cfirst)
(hcmax : 0 ≤ cmax)
(hM : 0 ≤ M)
(hconst : IsotropySlotConstants d g Cpre eta cRow kap (absorbedNormalizer cfirst cmax M) cD delta)
(hFnn : ∀ (j : ℕ), 0 ≤ hatExcess P q N₀ j)
(hFmono : ∀ (p j : ℕ), p ≤ j → hatExcess P q N₀ j ≤ hatExcess P q N₀ p)
{V : ℕ → ℕ → ℝ}
{V0 : ℕ → ℝ}
{Dr : ℕ → ℕ → ℝ}
{Vmean bmaj : ℕ → ℝ}
{beta lev : ℝ}
{wv : ℕ → ℝ}
{jb : ℕ → ℕ}
{cVsum cVm : ℝ}
{vsum vmsrc bsrc : ℕ → ℝ}
(hV : ∀ (n j : ℕ), 0 ≤ V n j)
(hV0 : ∀ (n : ℕ), 0 ≤ V0 n)
(hDrnn : ∀ (n j : ℕ), 0 ≤ Dr n j)
(hVmean0 : ∀ (n : ℕ), 0 ≤ Vmean n)
(hbmaj : ∀ (n : ℕ), 0 ≤ bmaj n)
(hbeta : 0 ≤ beta)
(hbad :
∀ (n : ℕ),
√2 * √(L + 1) * Response.profileBadMajorantAt 4 (bmaj n) beta lev + √2 * 3 ^ (-((1 - contrastRho g) / 2) * ↑(Hw n)) * √(L + 1) ≤ bsrc n)
(hH : ∀ (n : ℕ), ns ≤ n → H + 1 ≤ n)
(hHw : ∀ (n : ℕ), ns ≤ n → Hw n + 1 ≤ n)
(hjbn : ∀ (n : ℕ), ns ≤ n → jb n ≤ n)
(hmaj :
∀ (n : ℕ),
ns ≤ n →
wv n ≤ weakValueBaseIsotropyAtPar cfirst cmax M L (contrastRho g) (Hw n) (bmaj n) beta lev (V n) (V0 n) (Dr n)
(Vmean n) ^ 2)
(hone :
∀ (n : ℕ),
ns ≤ n →
adaptedHattedContrast P q (↑N₀ + ↑n) - 1 ≤ 4 * Cpre * ((3 / 2 + 1 / (4 * eta)) * (16 * ↑d * (adaptedHattedContrast P q (↑N₀ + ↑(n - H)) - adaptedHattedContrast P q (↑N₀ + ↑n))) + rowValue2Isotropy d cRow kap (↑d * (adaptedHattedContrast P q (↑N₀ + ↑n) - 1)) + wv n) + 2 * ((3 * ↑d + 4) * (↑d * (adaptedHattedContrast P q (↑N₀ + ↑n) - 1)) ^ 2))
(hVsum :
∀ (n : ℕ),
ns ≤ n →
∑ j ∈ Finset.range (Hw n + 1), 3 ^ (-(1 / 2) * ↑j) * (V n j + V0 n) ≤ vsum n + cVsum * hatExcess P q N₀ (jb n))
(hVmeanle : ∀ (n : ℕ), ns ≤ n → Vmean n ≤ vmsrc n + cVm * hatExcess P q N₀ (jb n))
(hDrdelta : ∀ (n : ℕ), ns ≤ n → ∀ j ∈ Finset.range (Hw n + 1), Dr n j ≤ delta)
(hDrdrop :
∀ (n : ℕ), ns ≤ n → ∀ j ∈ Finset.range (Hw n + 1), Dr n j ≤ cD * (hatExcess P q N₀ (n - j) - hatExcess P q N₀ n))
(n : ℕ)
:
ns ≤ n →
hatExcess P q N₀ n ≤ fusionRecursionConstantIsotropySharp d Cpre eta H (absorbedNormalizer cfirst cmax M) L g cRow kap cD delta cVsum
cVm * iterationDropSum (3 ^ (-recursionAlpha g)) (hatExcess P q N₀) n + fusionRecursionConstantIsotropySharp d Cpre eta H (absorbedNormalizer cfirst cmax M) L g cRow kap cD delta cVsum
cVm * hatExcess P q N₀ (jb n) ^ 2 + 3 * weakCoefficient d Cpre * weakSourceGroupSummed (absorbedNormalizer cfirst cmax M) L (contrastRho g) (vsum n) (vmsrc n) (bsrc n) ^ 2
The released-clause line producer with the source kept explicit.
theorem
HCPolySupport.HighContrast.Quenched.family_hrec_of_line_clauses_src
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{q : Mat d}
{N₀ ns H : ℕ}
{Hw : ℕ → ℕ}
{g Cpre eta cRow kap M L cD delta cfirst cmax : ℝ}
(hcfirst : 0 ≤ cfirst)
(hcmax : 0 ≤ cmax)
(hM : 0 ≤ M)
(hconst : IsotropySlotConstants d g Cpre eta cRow kap (absorbedNormalizer cfirst cmax M) cD delta)
(hFnn : ∀ (j : ℕ), 0 ≤ hatExcess P q N₀ j)
(hFmono : ∀ (p j : ℕ), p ≤ j → hatExcess P q N₀ j ≤ hatExcess P q N₀ p)
{V : ℕ → ℕ → ℕ → ℝ}
{V0 Dr Vmean : ℕ → ℕ → ℝ}
{bmaj : ℕ → ℝ}
{beta lev : ℝ}
{wv : ℕ → ℕ → ℝ}
{cVsum cVm : ℝ}
{vsum vmsrc : ℕ → ℕ → ℝ}
{bsrc : ℕ → ℝ}
(hV : ∀ (m n j : ℕ), 0 ≤ V m n j)
(hV0 : ∀ (m n : ℕ), 0 ≤ V0 m n)
(hDrnn : ∀ (n j : ℕ), 0 ≤ Dr n j)
(hVmean0 : ∀ (m n : ℕ), 0 ≤ Vmean m n)
(hbmaj : ∀ (n : ℕ), 0 ≤ bmaj n)
(hbeta : 0 ≤ beta)
(hbad :
∀ (n : ℕ),
√2 * √(L + 1) * Response.profileBadMajorantAt 4 (bmaj n) beta lev + √2 * 3 ^ (-((1 - contrastRho g) / 2) * ↑(Hw n)) * √(L + 1) ≤ bsrc n)
(hH : ∀ (n : ℕ), ns ≤ n → H + 1 ≤ n)
(hHw : ∀ (n : ℕ), ns ≤ n → Hw n + 1 ≤ n)
(hmaj :
∀ (m : ℕ),
ns ≤ m →
∀ (n : ℕ),
ns ≤ n →
wv m n ≤ weakValueBaseIsotropyAtPar cfirst cmax M L (contrastRho g) (Hw n) (bmaj n) beta lev (V m n) (V0 m n) (Dr n)
(Vmean m n) ^ 2)
(hone :
∀ (m : ℕ),
ns ≤ m →
∀ (n : ℕ),
ns ≤ n →
adaptedHattedContrast P q (↑N₀ + ↑n) - 1 ≤ 4 * Cpre * ((3 / 2 + 1 / (4 * eta)) * (16 * ↑d * (adaptedHattedContrast P q (↑N₀ + ↑(n - H)) - adaptedHattedContrast P q (↑N₀ + ↑n))) + rowValue2Isotropy d cRow kap (↑d * (adaptedHattedContrast P q (↑N₀ + ↑n) - 1)) + wv m n) + 2 * ((3 * ↑d + 4) * (↑d * (adaptedHattedContrast P q (↑N₀ + ↑n) - 1)) ^ 2))
(hVsum :
∀ (m : ℕ),
ns ≤ m →
∀ (n : ℕ),
ns ≤ n →
∑ j ∈ Finset.range (Hw n + 1), 3 ^ (-(1 / 2) * ↑j) * (V m n j + V0 m n) ≤ vsum m n + cVsum * hatExcess P q N₀ (min n m))
(hVmeanle : ∀ (m : ℕ), ns ≤ m → ∀ (n : ℕ), ns ≤ n → Vmean m n ≤ vmsrc m n + cVm * hatExcess P q N₀ (min n m))
(hDrdelta : ∀ (n : ℕ), ns ≤ n → ∀ j ∈ Finset.range (Hw n + 1), Dr n j ≤ delta)
(hDrdrop :
∀ (n : ℕ), ns ≤ n → ∀ j ∈ Finset.range (Hw n + 1), Dr n j ≤ cD * (hatExcess P q N₀ (n - j) - hatExcess P q N₀ n))
(n : ℕ)
:
ns ≤ n →
∀ (m : ℕ),
ns ≤ m →
m ≤ n →
hatExcess P q N₀ n ≤ fusionRecursionConstantIsotropySharp d Cpre eta H (absorbedNormalizer cfirst cmax M) L g cRow kap cD delta
cVsum cVm * iterationDropSum (3 ^ (-recursionAlpha g)) (hatExcess P q N₀) n + fusionRecursionConstantIsotropySharp d Cpre eta H (absorbedNormalizer cfirst cmax M) L g cRow kap cD delta
cVsum cVm * hatExcess P q N₀ m ^ 2 + 3 * weakCoefficient d Cpre * weakSourceGroupSummed (absorbedNormalizer cfirst cmax M) L (contrastRho g) (vsum m n) (vmsrc m n)
(bsrc n) ^ 2
The family block with the explicit source.