High-contrast homogenization: Provider.Quenched.SmallContrastHmajIsotropyAtLevel #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The hmaj slot at a released split level #
The value-side clause of the line producer, at the released weak value. The chain is the pinned one with three constants and one threshold pair carried as parameters: the metric-factor comparison, the isotropy carriers' instantiation, the generation-indexed family, and the law-free weakening of the normalizer.
The normalizer's linearity is what makes the last step work at any
coefficients: every group of the parametrized base carries the normalizer as a
factor, so the base is M times its value at M = 1.
The normalizer is a factor #
theorem
HCPolySupport.HighContrast.Quenched.weakValueBaseIsotropyAtPar_eq_mul
{d : ℕ}
(cfirst cmax M L rho : ℝ)
(Hw : ℕ)
(bmaj beta lev : ℝ)
(V : ℕ → ℝ)
(V0 : ℝ)
(Dr : ℕ → ℝ)
(Vmean : ℝ)
:
weakValueBaseIsotropyAtPar cfirst cmax M L rho Hw bmaj beta lev V V0 Dr Vmean = M * weakValueBaseIsotropyAtPar cfirst cmax 1 L rho Hw bmaj beta lev V V0 Dr Vmean
The parametrized base is linear in the normalizer.
theorem
HCPolySupport.HighContrast.Quenched.weakValueBaseIsotropyAtPar_mono_M
{d : ℕ}
{cfirst cmax M M' L rho : ℝ}
{Hw : ℕ}
{bmaj beta lev : ℝ}
{V : ℕ → ℝ}
{V0 : ℝ}
{Dr : ℕ → ℝ}
{Vmean : ℝ}
(hcfirst : 0 ≤ cfirst)
(hcmax : 0 ≤ cmax)
(hMM : M ≤ M')
(hrho1 : rho < 1)
(hbmaj : 0 ≤ bmaj)
(hbeta : 0 ≤ beta)
(hV : ∀ (j : ℕ), 0 ≤ V j)
(hV0 : 0 ≤ V0)
(hDr : ∀ (j : ℕ), 0 ≤ Dr j)
(hVmean : 0 ≤ Vmean)
:
weakValueBaseIsotropyAtPar cfirst cmax M L rho Hw bmaj beta lev V V0 Dr Vmean ≤ weakValueBaseIsotropyAtPar cfirst cmax M' L rho Hw bmaj beta lev V V0 Dr Vmean
The parametrized base is monotone in the normalizer.
The hmaj position at a released split level #
theorem
HCPolySupport.HighContrast.Quenched.weak_value_le_baseIsotropyAtPar_sq_at_scalar_at_level
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{E : BlockMat d}
{c kapc L rho bmaj beta lev cfirst cmax ctail : ℝ}
{Hw : ℕ}
{t l : ℤ}
{V : ℕ → ℝ}
{V0 : ℝ}
{Dr : ℕ → ℝ}
{Vmean : ℝ}
(hE : IsSymmetricBlockMat E)
(hEpd : Book.Ch02.BlockPosDef E)
(hsharp : BlockMatLoewnerLE (blockSharp E) E)
(hrec : canonicalShear E = 0)
{S0 SStar0 K0 : Mat d}
(hS0 : Matrix.PosDef S0)
(hStar0 : Matrix.PosDef SStar0)
(hform : toFullBlockMat (adaptedMean P (roundedGrid l (canonicalMetric E)) t) = schurBlock S0 SStar0 K0)
(hc : 0 ≤ c)
(hkapc : 0 ≤ kapc)
(henv : BlockMatLoewnerLE (adaptedMean P (roundedGrid l (canonicalMetric E)) t) (blockScale c E))
(hcomp : BlockMatLoewnerLE E (blockScale kapc (adaptedMean P (roundedGrid l (canonicalMetric E)) t)))
(hcfirst : 0 ≤ cfirst)
(hcmax : 0 ≤ cmax)
(hctail : √2 ≤ ctail)
(hrho1 : rho < 1)
(hV : ∀ (j : ℕ), 0 ≤ V j)
(hV0 : 0 ≤ V0)
(hDr : ∀ (j : ℕ), 0 ≤ Dr j)
(hVmean : 0 ≤ Vmean)
(hbad : 0 ≤ bmaj)
(hbeta : 0 ≤ beta)
:
weakValueBoundSharpIsotropyAt cfirst cmax ctail P (canonicalMetric E) (Response.responseSkew K0) (blockScale c E) L
(canonicalMetric E) rho Hw bmaj beta lev t l V V0 Dr Vmean ≤ weakValueBaseIsotropyAtPar cfirst (cmax * ctail) (metricFactorValue E c kapc) L rho Hw bmaj beta lev V V0 Dr Vmean ^ 2
The hmaj position at an abstract envelope scalar, released.
theorem
HCPolySupport.HighContrast.Quenched.weak_value_le_baseIsotropyAtPar_sq_at_isotropy_at_level
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{E : BlockMat d}
{cIso kap rho bmaj beta lev cfirst cmax ctail : ℝ}
{Hw : ℕ}
{t l : ℤ}
{V : ℕ → ℝ}
{V0 : ℝ}
{Dr : ℕ → ℝ}
{Vmean : ℝ}
(hE : IsSymmetricBlockMat E)
(hEpd : Book.Ch02.BlockPosDef E)
(hsharp : BlockMatLoewnerLE (blockSharp E) E)
(hrec : canonicalShear E = 0)
{S0 SStar0 K0 : Mat d}
(hS0 : Matrix.PosDef S0)
(hStar0 : Matrix.PosDef SStar0)
(hform : toFullBlockMat (adaptedMean P (roundedGrid l (canonicalMetric E)) t) = schurBlock S0 SStar0 K0)
(hcIso : 0 ≤ cIso)
(hsmall : cIso < 1)
(henv : BlockMatLoewnerLE (adaptedMean P (roundedGrid l (canonicalMetric E)) t) (isotropyReference cIso E))
(hcomp : BlockMatLoewnerLE E (blockScale (isotropyKap2 cIso) (adaptedMean P (roundedGrid l (canonicalMetric E)) t)))
(hcfirst : 0 ≤ cfirst)
(hcmax : 0 ≤ cmax)
(hctail : √2 ≤ ctail)
(hrho1 : rho < 1)
(hV : ∀ (j : ℕ), 0 ≤ V j)
(hV0 : 0 ≤ V0)
(hDr : ∀ (j : ℕ), 0 ≤ Dr j)
(hVmean : 0 ≤ Vmean)
(hbad : 0 ≤ bmaj)
(hbeta : 0 ≤ beta)
:
weakValueBoundSharpIsotropyAt cfirst cmax ctail P (canonicalMetric E) (Response.responseSkew K0)
(isotropyReference cIso E) (isotropyLoadScale cIso kap) (canonicalMetric E) rho Hw bmaj beta lev t l V V0 Dr Vmean ≤ weakValueBaseIsotropyAtPar cfirst (cmax * ctail) (metricFactorValue E (1 + cIso) (isotropyKap2 cIso))
(isotropyLoadScale cIso kap) rho Hw bmaj beta lev V V0 Dr Vmean ^ 2
The hmaj position at the isotropy carriers, released.
theorem
HCPolySupport.HighContrast.Quenched.hmaj_at_isotropy_at_level
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{E : BlockMat d}
(hE : IsSymmetricBlockMat E)
(hEpd : Book.Ch02.BlockPosDef E)
(hsharp : BlockMatLoewnerLE (blockSharp E) E)
(hrec : canonicalShear E = 0)
{cIso rho : ℝ}
(hcIso : 0 ≤ cIso)
(hcsmall : cIso < 1)
(hrho1 : rho < 1)
{Hw : ℕ}
{lAl : ℤ}
{N₀ : ℕ}
{S0 SStar0 K0 : ℕ → Mat d}
(hS0 : ∀ (n : ℕ), Matrix.PosDef (S0 n))
(hStar0 : ∀ (n : ℕ), Matrix.PosDef (SStar0 n))
(hform :
∀ (n : ℕ),
toFullBlockMat (adaptedMean P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑n)) = schurBlock (S0 n) (SStar0 n) (K0 n))
(henv :
∀ (n : ℕ),
BlockMatLoewnerLE (adaptedMean P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑n)) (isotropyReference cIso E))
(hcomp :
∀ (n : ℕ),
BlockMatLoewnerLE E
(blockScale (isotropyKap2 cIso) (adaptedMean P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑n))))
{V : ℕ → ℕ → ℝ}
{V0 : ℕ → ℝ}
{Dr : ℕ → ℕ → ℝ}
{Vmean bmaj : ℕ → ℝ}
{beta lev cfirst cmax ctail : ℝ}
(hV : ∀ (n j : ℕ), 0 ≤ V n j)
(hV0 : ∀ (n : ℕ), 0 ≤ V0 n)
(hDr : ∀ (n j : ℕ), 0 ≤ Dr n j)
(hVmean : ∀ (n : ℕ), 0 ≤ Vmean n)
(hbmaj : ∀ (n : ℕ), 0 ≤ bmaj n)
(hbeta : 0 ≤ beta)
(hcfirst : 0 ≤ cfirst)
(hcmax : 0 ≤ cmax)
(hctail : √2 ≤ ctail)
(n : ℕ)
:
weakValueBoundSharpIsotropyAt cfirst cmax ctail P (canonicalMetric E) (Response.responseSkew (K0 n))
(isotropyReference cIso E) (isotropyLoadScale cIso (isotropyKap2 cIso)) (canonicalMetric E) rho Hw (bmaj n) beta lev
(↑N₀ + ↑n) lAl (V n) (V0 n) (Dr n) (Vmean n) ≤ weakValueBaseIsotropyAtPar cfirst (cmax * ctail) (metricFactorValue E (1 + cIso) (isotropyKap2 cIso))
(isotropyLoadScale cIso (isotropyKap2 cIso)) rho Hw (bmaj n) beta lev (V n) (V0 n) (Dr n) (Vmean n) ^ 2
hmaj at the isotropy carriers, released.
theorem
HCPolySupport.HighContrast.Quenched.hmaj_at_isotropy_of_metric_bound_at_level
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{E : BlockMat d}
(hE : IsSymmetricBlockMat E)
(hEpd : Book.Ch02.BlockPosDef E)
(hsharp : BlockMatLoewnerLE (blockSharp E) E)
(hrec : canonicalShear E = 0)
{cIso rho : ℝ}
(hcIso : 0 ≤ cIso)
(hcsmall : cIso < 1)
(hrho1 : rho < 1)
{Hw : ℕ}
{lAl : ℤ}
{N₀ : ℕ}
{S0 SStar0 K0 : ℕ → Mat d}
(hS0 : ∀ (n : ℕ), Matrix.PosDef (S0 n))
(hStar0 : ∀ (n : ℕ), Matrix.PosDef (SStar0 n))
(hform :
∀ (n : ℕ),
toFullBlockMat (adaptedMean P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑n)) = schurBlock (S0 n) (SStar0 n) (K0 n))
(henv :
∀ (n : ℕ),
BlockMatLoewnerLE (adaptedMean P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑n)) (isotropyReference cIso E))
(hcomp :
∀ (n : ℕ),
BlockMatLoewnerLE E
(blockScale (isotropyKap2 cIso) (adaptedMean P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑n))))
{V : ℕ → ℕ → ℝ}
{V0 : ℕ → ℝ}
{Dr : ℕ → ℕ → ℝ}
{Vmean bmaj : ℕ → ℝ}
{beta lev cfirst cmax ctail : ℝ}
(hV : ∀ (n j : ℕ), 0 ≤ V n j)
(hV0 : ∀ (n : ℕ), 0 ≤ V0 n)
(hDr : ∀ (n j : ℕ), 0 ≤ Dr n j)
(hVmean : ∀ (n : ℕ), 0 ≤ Vmean n)
(hbmaj : ∀ (n : ℕ), 0 ≤ bmaj n)
(hbeta : 0 ≤ beta)
(hcfirst : 0 ≤ cfirst)
(hcmax : 0 ≤ cmax)
(hctail : √2 ≤ ctail)
{M' : ℝ}
(hM' : metricFactorValue E (1 + cIso) (isotropyKap2 cIso) ≤ M')
(n : ℕ)
:
weakValueBoundSharpIsotropyAt cfirst cmax ctail P (canonicalMetric E) (Response.responseSkew (K0 n))
(isotropyReference cIso E) (isotropyLoadScale cIso (isotropyKap2 cIso)) (canonicalMetric E) rho Hw (bmaj n) beta lev
(↑N₀ + ↑n) lAl (V n) (V0 n) (Dr n) (Vmean n) ≤ weakValueBaseIsotropyAtPar cfirst (cmax * ctail) M' (isotropyLoadScale cIso (isotropyKap2 cIso)) rho Hw (bmaj n) beta
lev (V n) (V0 n) (Dr n) (Vmean n) ^ 2
hmaj at a law-free normalizer, released. The normalizer is weakened
to any upper bound, which is what the endpoint's binder requires of it.