High-contrast homogenization: Entry.ParentChildRecurrence #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Exact parent–child recurrence #
Under the standing ellipticity threshold, the localised quotient Schatten norm of the
normalised fluctuation at the parent scale is bounded by its value at the child scale,
multiplied by the exponential of the determinant increment and the two printed scale
factors, with the source constant of the matrix-averaging statement. This is the exact
parent–child recurrence of p.fixed.geometry.parent.child.recurrence, with the mean
positive-definiteness and finite-moment premises discharged from the two printed constants
without slack.
theorem
HCPolySupport.HighContrast.Entry.fixed_geometry_parent_child_recurrence
(d : ℕ)
(hd : 2 ≤ d)
(γ : ℝ)
(hγ : γ ∈ Set.Ico 0 1)
:
∃ (Csrc : ℝ),
0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ),
MeasureTheory.IsProbabilityMeasure P →
IsStationaryLaw P →
IsUnitRangeLaw P →
CoarseEllipticityDagger P γ E Ψ K S →
∀ (N : ℕ),
2 ≤ N →
Even N →
∀ (jStar : ℕ),
2 * d ≤ 3 ^ jStar →
⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar →
∀ (m : Mat d),
Matrix.PosDef m →
∀ (j h : ℤ),
↑jStar ≤ j →
1 ≤ h →
lqSchattenNorm P (↑N)
(normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar m) (j + h)) ≤ ↑N * 3 ^ (↑d / 2) * (1 + (2 * ↑d) ^ (↑N)⁻¹) * 3 ^ (-(↑d / 2) * ↑h) * Real.exp (detIncrement P (Geometry.explicitRoundedGrid jStar m) j (j + h)) * lqSchattenNorm P (↑N)
(normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar m) j) + 2 * (1 + ↑d ^ (1 - (↑N)⁻¹)) * Real.exp
((1 - (↑N)⁻¹) * detIncrement P (Geometry.explicitRoundedGrid jStar m) j (j + h)) * (Real.exp (detIncrement P (Geometry.explicitRoundedGrid jStar m) j (j + h)) - 1) ^ (↑N)⁻¹
The exact printed recurrence, near p.fixed.geometry.parent.child.recurrence.