Coarse-graining support: Support.Besov.Duality.ProjectionLimit

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

theorem HCPolySupport.integrableOn_cubeProjection_of_integrableOn {d : ℕ} (Q : TriadicCube d) (j : ℕ) (g : Vec d → ℝ) : MeasureTheory.IntegrableOn (cubeProjection Q j g) (cubeSet Q) MeasureTheory.volume

theorem HCPolySupport.cubeProjection_abs_le_of_abs_le_on_cubeSet {d : ℕ} (Q : TriadicCube d) (j : ℕ) (g : Vec d → ℝ) (C : ℝ) (hbound : ∀ x ∈ cubeSet Q, |g x| ≤ C) (x : Vec d) : x ∈ cubeSet Q → |cubeProjection Q j g x| ≤ C

theorem HCPolySupport.cubeBesovPairing_projection_comm {d : ℕ} (Q : TriadicCube d) (j : ℕ) (u g : Vec d → ℝ) (huInt : MeasureTheory.IntegrableOn u (cubeSet Q) MeasureTheory.volume) (hgInt : MeasureTheory.IntegrableOn g (cubeSet Q) MeasureTheory.volume) : cubeBesovPairing Q (cubeProjection Q j u) g = cubeBesovPairing Q u (cubeProjection Q j g)

theorem HCPolySupport.tendsto_cubeBesovPairing_projection_right_of_integrableOn_of_bounded {d : ℕ} (Q : TriadicCube d) (u g : Vec d → ℝ) (C : ℝ) (huInt : MeasureTheory.IntegrableOn u (cubeSet Q) MeasureTheory.volume) (hgInt : MeasureTheory.IntegrableOn g (cubeSet Q) MeasureTheory.volume) (hC : 0 ≤ C) (hbound : ∀ x ∈ cubeSet Q, |g x| ≤ C) : Filter.Tendsto (fun (n : ℕ) => cubeBesovPairing Q u (cubeProjection Q (n + 1) g)) Filter.atTop (nhds (cubeBesovPairing Q u g))

theorem HCPolySupport.tendsto_cubeBesovPairing_projection_left_of_integrableOn_of_bounded {d : ℕ} (Q : TriadicCube d) (u g : Vec d → ℝ) (C : ℝ) (huInt : MeasureTheory.IntegrableOn u (cubeSet Q) MeasureTheory.volume) (hgInt : MeasureTheory.IntegrableOn g (cubeSet Q) MeasureTheory.volume) (hC : 0 ≤ C) (hbound : ∀ x ∈ cubeSet Q, |g x| ≤ C) : Filter.Tendsto (fun (n : ℕ) => cubeBesovPairing Q (cubeProjection Q (n + 1) u) g) Filter.atTop (nhds (cubeBesovPairing Q u g))

theorem HCPolySupport.normalizedCubeMeasure_descendant_eq_smul_restrict {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) : normalizedCubeMeasure R = ENNReal.ofReal (cubeVolume Q / cubeVolume R) • (normalizedCubeMeasure Q).restrict (cubeSet R)

theorem HCPolySupport.memLp_on_descendant_of_memLp {d : ℕ} {Q R : TriadicCube d} {j : ℕ} {p : ENNReal} {f : Vec d → ℝ} (hR : R ∈ descendantsAtDepth Q j) (hf : MeasureTheory.MemLp f p (normalizedCubeMeasure Q)) : MeasureTheory.MemLp f p (normalizedCubeMeasure R)

theorem HCPolySupport.cubeBesovCircDepthAverage_le_cubeLpNorm_rpow {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (j : ℕ) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) : cubeBesovCircDepthAverage Q p u j ≤ cubeLpNorm Q p u ^ p.toReal

theorem HCPolySupport.cubeProjection_memLp {d : ℕ} (Q : TriadicCube d) (j : ℕ) (p : ENNReal) (u : Vec d → ℝ) : MeasureTheory.MemLp (cubeProjection Q j u) p (normalizedCubeMeasure Q)

theorem HCPolySupport.cubeLpNorm_rpow_cubeProjection_eq_cubeBesovCircDepthAverage {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (j : ℕ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) : cubeLpNorm Q p (cubeProjection Q j u) ^ p.toReal = cubeBesovCircDepthAverage Q p u j

theorem HCPolySupport.cubeLpNorm_cubeProjection_le {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (j : ℕ) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) : cubeLpNorm Q p (cubeProjection Q j u) ≤ cubeLpNorm Q p u

theorem HCPolySupport.cubeBesovPairing_sub_right_of_integrableOn {d : ℕ} (Q : TriadicCube d) (f g h : Vec d → ℝ) (hfg : MeasureTheory.IntegrableOn (fun (x : Vec d) => f x * g x) (cubeSet Q) MeasureTheory.volume) (hfh : MeasureTheory.IntegrableOn (fun (x : Vec d) => f x * h x) (cubeSet Q) MeasureTheory.volume) : (cubeBesovPairing Q f fun (x : Vec d) => g x - h x) = cubeBesovPairing Q f g - cubeBesovPairing Q f h

theorem HCPolySupport.tendsto_cubeBesovPairing_projection_left_of_memLp {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u g : Vec d → ℝ) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g (cubeBesovConjExponent p) (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hpConjTop : cubeBesovConjExponent p ≠ ⊤) : Filter.Tendsto (fun (n : ℕ) => cubeBesovPairing Q (cubeProjection Q (n + 1) u) g) Filter.atTop (nhds (cubeBesovPairing Q u g))