Coarse-graining support: Support.Besov.Poincare.HarmonicGradient.Descendants

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Descendant APIs for Vector Poincare Estimates

theorem HCPolySupport.CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate.mono_C {d : ℕ} {Q : TriadicCube d} {C₁ C₂ : ℝ} {u : Vec d → ℝ} {G : Vec d → Vec d} {M : ℕ} (h : CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate Q C₁ u G M) (hC : C₁ ≤ C₂) : CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate Q C₂ u G M

Enlarge the constant in the projected vector Poincare estimate.

theorem HCPolySupport.CubeProjectedDualMeanZeroVectorPoincareEstimate.to_descendant {d : ℕ} {Q : TriadicCube d} {C : ℝ} {u : Vec d → ℝ} {G : Vec d → Vec d} {M : ℕ} (hu : ∀ j ∈ Finset.range (M + 1), ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) (hlocal : ∀ j ∈ Finset.range (M + 1), ∀ R ∈ descendantsAtDepth Q j, CubeProjectedDualMeanZeroVectorPoincareEstimate R C u G (M - j)) : CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate Q C (cubeFluctuation Q u) G M

Assemble descendant projected vector Poincare from one-cube projected estimates on every descendant. The only rewrite is that subtracting the parent cube average does not change oscillation on the descendant.

theorem HCPolySupport.CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate.restrict_to_descendant {d : ℕ} {Q R : TriadicCube d} {C : ℝ} {u : Vec d → ℝ} {G : Vec d → Vec d} {M j : ℕ} (hproj : CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate Q C u G M) (hR : R ∈ descendantsAtDepth Q j) (hj : j ≤ M) : CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate R C u G (M - j)

Restrict a descendant projected vector Poincare estimate to one of the parent cube's descendants. The depth bookkeeping is the same as in the scalar projected Poincare corridor: a depth-n descendant of R is a depth-j + n descendant of Q.

theorem HCPolySupport.CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate.restrict_fluctuation_to_descendant {d : ℕ} {Q R : TriadicCube d} {C : ℝ} {u : Vec d → ℝ} {G : Vec d → Vec d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (hu : ∀ (n : ℕ), ∀ S ∈ descendantsAtDepth R n, MeasureTheory.MemLp u 2 (normalizedCubeMeasure S)) (hproj : ∀ (M : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate Q C (cubeFluctuation Q u) G M) (N : ℕ) : CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate R C (cubeFluctuation R u) G N

Localize a parent cube projected vector Poincare family to a descendant cube while recentering the fluctuation from the parent average to the local descendant average.

theorem HCPolySupport.CubeDualMeanZeroVectorPoincareEstimate.to_descendant {d : ℕ} {Q : TriadicCube d} {C : ℝ} {u : Vec d → ℝ} {G : Vec d → Vec d} {M : ℕ} (hu : ∀ j ∈ Finset.range (M + 1), ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) (hlocal : ∀ j ∈ Finset.range (M + 1), ∀ R ∈ descendantsAtDepth Q j, CubeDualMeanZeroVectorPoincareEstimate R C u G) : CubeDescendantDualMeanZeroVectorPoincareEstimate Q C (cubeFluctuation Q u) G M

Assemble the descendant infinite-depth vector Poincare estimate from one-cube infinite-depth estimates on every descendant.

theorem HCPolySupport.CubeDualFullVectorPoincareEstimate.to_descendant {d : ℕ} {Q : TriadicCube d} {C : ℝ} {u : Vec d → ℝ} {G : Vec d → Vec d} {M : ℕ} (hu : ∀ j ∈ Finset.range (M + 1), ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) (hlocal : ∀ j ∈ Finset.range (M + 1), ∀ R ∈ descendantsAtDepth Q j, CubeDualFullVectorPoincareEstimate R C u G) : CubeDescendantDualFullVectorPoincareEstimate Q C (cubeFluctuation Q u) G M

Assemble the descendant full-dual vector Poincare estimate from one-cube full-dual estimates on every descendant.

theorem HCPolySupport.CubeDescendantDualFullVectorPoincareEstimate.mono_C {d : ℕ} {Q : TriadicCube d} {C₁ C₂ : ℝ} {u : Vec d → ℝ} {G : Vec d → Vec d} {M : ℕ} (hfull : CubeDescendantDualFullVectorPoincareEstimate Q C₁ u G M) (hC : C₁ ≤ C₂) : CubeDescendantDualFullVectorPoincareEstimate Q C₂ u G M

Enlarge the constant in the descendant full-dual vector Poincare estimate.

theorem HCPolySupport.CubeDescendantDualFullVectorPoincareEstimate.restrict_to_descendant {d : ℕ} {Q R : TriadicCube d} {C : ℝ} {u : Vec d → ℝ} {G : Vec d → Vec d} {M j : ℕ} (hfull : CubeDescendantDualFullVectorPoincareEstimate Q C u G M) (hR : R ∈ descendantsAtDepth Q j) (hj : j ≤ M) : CubeDescendantDualFullVectorPoincareEstimate R C u G (M - j)

Restrict a descendant full-dual vector Poincare estimate to one of the parent cube's descendants.

theorem HCPolySupport.CubeDescendantDualFullVectorPoincareEstimate.restrict_fluctuation_to_descendant {d : ℕ} {Q R : TriadicCube d} {C : ℝ} {u : Vec d → ℝ} {G : Vec d → Vec d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (hu : ∀ (n : ℕ), ∀ S ∈ descendantsAtDepth R n, MeasureTheory.MemLp u 2 (normalizedCubeMeasure S)) (hfull : ∀ (M : ℕ), CubeDescendantDualFullVectorPoincareEstimate Q C (cubeFluctuation Q u) G M) (N : ℕ) : CubeDescendantDualFullVectorPoincareEstimate R C (cubeFluctuation R u) G N

Localize a parent cube full-dual vector Poincare family to a descendant cube while recentering the fluctuation from the parent average to the local descendant average.