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

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

def HCPolySupport.CubeDescendantProjectedDualMeanZeroPoincareEstimate {d : ℕ} (Q : TriadicCube d) (C : ℝ) (u g : Vec d → ℝ) (M : ℕ) : Prop

Descendant-local analytic hypothesis where the local dual mean-zero Poincare estimate is supplied against the finite projection of g on each descendant cube at the exact depth that matches the multiscale corridor's M - j indexing.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.CubeDescendantProjectedDualMeanZeroPoincareEstimate.to_localEstimate {d : ℕ} {Q : TriadicCube d} {C : ℝ} {u g : Vec d → ℝ} {M : ℕ} (hproj : CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C u g M) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hC : 0 ≤ C) : CubeLocalMultiscalePoincareEstimate Q (3 / 2 * C * 3 ^ (↑d + 1)) u g M

theorem HCPolySupport.CubeDescendantProjectedDualMeanZeroPoincareEstimate.to_input {d : ℕ} {Q : TriadicCube d} {C : ℝ} {u g : Vec d → ℝ} {M : ℕ} (hproj : CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C u g M) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hC : 0 ≤ C) : CubeMultiscalePoincareInput Q (3 / 2 * C * 3 ^ (↑d + 1)) u g M

theorem HCPolySupport.cubeBesovCircDepthWeight_eq_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (s : ℝ) (n : ℕ) : cubeBesovCircDepthWeight R s n = cubeBesovCircDepthWeight Q s (j + n)

theorem HCPolySupport.sq_cubeBesovCircDepthSeminorm_two {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → ℝ) (j : ℕ) : cubeBesovCircDepthSeminorm Q s 2 u j ^ 2 = cubeBesovCircDepthWeight Q s j ^ 2 * cubeBesovCircDepthAverage Q 2 u j

theorem HCPolySupport.descendantsAverage_sq_cubeBesovCircDepthSeminorm_eq_shifted {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (j n : ℕ) : (descendantsAverage Q j fun (R : TriadicCube d) => cubeBesovCircDepthSeminorm R 1 2 u n ^ 2) = cubeBesovCircDepthSeminorm Q 1 2 u (j + n) ^ 2

theorem HCPolySupport.descendantsAverage_L2_sum_le_sum_descendantsAverage_L2 {d : ℕ} {ι : Type u_1} (Q : TriadicCube d) (j : ℕ) (s : Finset ι) (A : TriadicCube d → ι → ℝ) (hA : ∀ R ∈ descendantsAtDepth Q j, ∀ i ∈ s, 0 ≤ A R i) : (descendantsAverage Q j fun (R : TriadicCube d) => (∑ i ∈ s, A R i) ^ 2) ^ (1 / 2) ≤ ∑ i ∈ s, (descendantsAverage Q j fun (R : TriadicCube d) => A R i ^ 2) ^ (1 / 2)

theorem HCPolySupport.cubeBesovDepthSeminorm_two_le_sum_shifted_of_local_circ_bound {d : ℕ} (Q : TriadicCube d) (s C : ℝ) (u g : Vec d → ℝ) (j N : ℕ) (hC : 0 ≤ C) (hlocal : ∀ R ∈ descendantsAtDepth Q j, cubeBesovOscillation R 2 u ≤ C * ∑ n ∈ Finset.range (N + 1), cubeBesovCircDepthSeminorm R 1 2 g n) : cubeBesovDepthSeminorm Q s 2 u j ≤ C * cubeBesovDepthWeight Q s j * ∑ n ∈ Finset.range (N + 1), cubeBesovCircDepthSeminorm Q 1 2 g (j + n)

theorem HCPolySupport.shifted_cubeBesovCircDepthSum_le_cubeBesovCircPartialNorm_one {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (j N : ℕ) (u : Vec d → ℝ) : ∑ n ∈ Finset.range (N + 1), cubeBesovCircDepthSeminorm Q s p u (j + n) ≤ cubeBesovCircPartialNorm Q s p 1 (j + N) u