Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.InputSpecializations .SolutionInputs
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.thetaRatio_pos_of_closedCubeHarmonicFamily
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t : ℝ)
{lam Lam : ℝ}
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(hs : 0 < s)
(ht : 0 < t)
(hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a)
: