High-contrast homogenization: Provider.PolynomialHomogenization.Root.CorrectorDecay.LpTriangle #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.cubeLpNorm_sub_le
{d : ℕ}
(Q : TriadicCube d)
(f h : Vec d → ℝ)
(hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q))
(hh : MeasureTheory.MemLp h 2 (normalizedCubeMeasure Q))
:
The normalized cube L² triangle inequality in subtraction form.
theorem
HCPolySupport.HighContrast.memLp_originCube_pred
{d : ℕ}
(m : ℤ)
(f : Vec d → ℝ)
(hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure (originCube d m)))
:
MeasureTheory.MemLp f 2 (normalizedCubeMeasure (originCube d (m - 1)))
Restriction from a centered cube to its central child preserves L²
integrability for the normalized measures.
theorem
HCPolySupport.HighContrast.cubeLpNorm_originCube_pred_le
{d : ℕ}
(m : ℤ)
(f : Vec d → ℝ)
(hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure (originCube d m)))
:
The normalized child L² norm costs at most the child count.
theorem
HCPolySupport.HighContrast.weightedCubeLpNorm_originCube_pred_le
{d : ℕ}
(m : ℤ)
(f : Vec d → ℝ)
(W : ℝ)
(hW : 0 ≤ W)
(hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure (originCube d m)))
:
The same child restriction after multiplication by a nonnegative scale weight.
theorem
HCPolySupport.HighContrast.weightedSuccessorPrice_le
{d : ℕ}
(m : ℤ)
(f0 f1 w : Vec d → ℝ)
(Wpred Wmid Wsucc B0 B1 : ℝ)
(hw : w = fun (x : Vec d) => f1 x - f0 x)
(hf0 : MeasureTheory.MemLp f0 2 (normalizedCubeMeasure (originCube d m)))
(hf1 : MeasureTheory.MemLp f1 2 (normalizedCubeMeasure (originCube d m)))
(hWpred : 0 ≤ Wpred)
(hpredMid : Wpred = 3 * Wmid)
(hmidSucc : Wmid = 3 * Wsucc)
(h0 : Wmid * cubeLpNorm (originCube d (m - 1)) 2 f0 ≤ B0)
(h1 : Wsucc * cubeLpNorm (originCube d m) 2 f1 ≤ B1)
:
Abstract weighted bookkeeping for a successor represented as a difference of two consecutive fields.