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

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

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

Descendant-local analytic input for the finite-depth multiscale Poincare corridor.

Equations

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

theorem HCPolySupport.CubeMultiscalePoincareInput.bound {d : ℕ} {Q : TriadicCube d} {C : ℝ} {u g : Vec d → ℝ} {M : ℕ} (hinput : CubeMultiscalePoincareInput Q C u g M) (j : ℕ) : j ∈ Finset.range (M + 1) → ∀ R ∈ descendantsAtDepth Q j, cubeBesovOscillation R 2 u ≤ C * ∑ n ∈ Finset.range (M - j + 1), cubeBesovCircDepthSeminorm R 1 2 g n

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

Concrete descendant-local multiscale Poincare hypothesis phrased with the q = 1 concrete circ norm on each descendant cube.

Equations

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

theorem HCPolySupport.CubeLocalMultiscalePoincareEstimate.to_input {d : ℕ} {Q : TriadicCube d} {C : ℝ} {u g : Vec d → ℝ} {M : ℕ} (hlocal : CubeLocalMultiscalePoincareEstimate Q C u g M) : CubeMultiscalePoincareInput Q C u g M

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

Single-cube analytic Poincare estimate phrased with the true dual mean-zero negative Besov seminorm at the s = 1, p = 2, q = 1 endpoint. This is the black-box form of the note's l.multiscale.Poincare.function.spaces before passing to the concrete circ norm.

Equations

• HCPolySupport.CubeDualMeanZeroPoincareEstimate Q C u g = (HCPolySupport.cubeBesovOscillation Q 2 u ≤ C * HCPolySupport.cubeBesovDualMeanZeroSeminorm Q 1 2 1 g)

theorem HCPolySupport.CubeDualMeanZeroPoincareEstimate.to_circNorm {d : ℕ} {Q : TriadicCube d} {C : ℝ} {u g : Vec d → ℝ} (hdual : CubeDualMeanZeroPoincareEstimate Q C u g) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hC : 0 ≤ C) : cubeBesovOscillation Q 2 u ≤ C * 3 ^ (↑d + 1) * cubeBesovCircNorm Q 1 2 1 g

theorem HCPolySupport.CubeDualMeanZeroPoincareEstimate.fluctuation_le_circNorm {d : ℕ} {Q : TriadicCube d} {C : ℝ} {u g : Vec d → ℝ} (hdual : CubeDualMeanZeroPoincareEstimate Q C u g) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hC : 0 ≤ C) : cubeLpNorm Q 2 (cubeFluctuation Q u) ≤ C * 3 ^ (↑d + 1) * cubeBesovCircNorm Q 1 2 1 g

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

Descendant-local analytic input packaging the single-cube dual mean-zero Poincare estimate together with the local L² admissibility and the finite-depth comparison from the full circ norm to the concrete q = 1 partial circ norm on each descendant. This is the theorem-surface bridge from the single-cube analytic lemma to CubeLocalMultiscalePoincareEstimate.

Equations

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

theorem HCPolySupport.CubeDescendantDualMeanZeroPoincareInput.to_localEstimate {d : ℕ} {Q : TriadicCube d} {C K : ℝ} {u g : Vec d → ℝ} {M : ℕ} (hinput : CubeDescendantDualMeanZeroPoincareInput Q C K u g M) (hC : 0 ≤ C) : CubeLocalMultiscalePoincareEstimate Q (C * 3 ^ (↑d + 1) * K) u g M

theorem HCPolySupport.CubeDescendantDualMeanZeroPoincareInput.to_input {d : ℕ} {Q : TriadicCube d} {C K : ℝ} {u g : Vec d → ℝ} {M : ℕ} (hinput : CubeDescendantDualMeanZeroPoincareInput Q C K u g M) (hC : 0 ≤ C) : CubeMultiscalePoincareInput Q (C * 3 ^ (↑d + 1) * K) u g M