High-contrast homogenization: Provider.Quenched.RestoredSource #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Restoration of the microscopic source scale #
This file isolates the rescaled source scale of the dilated law and its tail, as
they are used in ss.algebraic.convergence. The tail event
is strict, exactly as in CoarseEllipticityDagger.source_tail and in the
reference text.
theorem
HCPolySupport.HighContrast.Quenched.measureReal_restored_source_upperTail_le
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{g : ℝ}
{E : BlockMat d}
{Ψ : ℝ → ℝ}
{K : ℝ}
{S : CoeffSpace d → ℝ}
(hdagger : CoarseEllipticityDagger P g E Ψ K S)
(Nann : ℕ)
{t : ℝ}
(ht : 1 ≤ t)
:
P.real (IndependentSums.upperTailEvent (fun (a : CoeffSpace d) => max 1 (S a / 3 ^ Nann)) t) ≤ (Ψ (3 ^ Nann * t))⁻¹
The restored source has the native tail at the dilated gauge argument.
The floor at one cannot contribute because the tail threshold is at least one and the upper-tail event is strict.
theorem
HCPolySupport.HighContrast.Quenched.exists_restored_source_scale
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{g : ℝ}
{E : BlockMat d}
{Ψ : ℝ → ℝ}
{K : ℝ}
{S : CoeffSpace d → ℝ}
(hdagger : CoarseEllipticityDagger P g E Ψ K S)
(Nann : ℕ)
:
∃ (Ssrc : CoeffSpace d → ℝ),
Measurable Ssrc ∧ (∀ (a : CoeffSpace d), 1 ≤ Ssrc a) ∧ (∀ (a : CoeffSpace d), Ssrc a = max 1 (S a / 3 ^ Nann)) ∧ ∀ (t : ℝ), 1 ≤ t → P.real (IndependentSums.upperTailEvent Ssrc t) ≤ (Ψ t)⁻¹
The restored microscopic source scale is measurable, at least one, and has the source-gauge upper tail after discarding the dilation factor by monotonicity.