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

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

theorem HCPolySupport.geom_sum_range_le_of_lt_one {x : ℝ} {n : ℕ} (hx : 0 ≤ x) (hx1 : x < 1) : ∑ i ∈ Finset.range n, x ^ i ≤ (1 - x)⁻¹

theorem HCPolySupport.sum_mul_le_mul_sum_of_nonneg {ι : Type u_1} {s : Finset ι} {f g : ι → ℝ} (hf : ∀ i ∈ s, 0 ≤ f i) (hg : ∀ i ∈ s, 0 ≤ g i) : ∑ i ∈ s, f i * g i ≤ s.sum f * s.sum g

theorem HCPolySupport.descendantsAverage_add_eq_descendantsAverage_descendantsAverage {d : ℕ} (Q : TriadicCube d) (j n : ℕ) (F : TriadicCube d → ℝ) : descendantsAverage Q (j + n) F = descendantsAverage Q j fun (R : TriadicCube d) => descendantsAverage R n F

theorem HCPolySupport.mem_descendantsAtDepth_add {d : ℕ} {Q R S : TriadicCube d} {j n : ℕ} (hR : R ∈ descendantsAtDepth Q j) (hS : S ∈ descendantsAtDepth R n) : S ∈ descendantsAtDepth Q (j + n)

theorem HCPolySupport.cubeProjection_add_eq_cubeProjection_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j n : ℕ} (f : Vec d → ℝ) {x : Vec d} (hR : R ∈ descendantsAtDepth Q j) (hx : x ∈ cubeSet R) : cubeProjection Q (j + n) f x = cubeProjection R n f x

theorem HCPolySupport.cubeAverage_cubeProjection_eq_cubeAverage_of_memLp {d : ℕ} (Q : TriadicCube d) (j : ℕ) (u : Vec d → ℝ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : cubeAverage Q (cubeProjection Q j u) = cubeAverage Q u

theorem HCPolySupport.cubeAverage_cubeProjection_add_eq_cubeAverage_of_mem_descendantsAtDepth_of_memLp {d : ℕ} {Q R : TriadicCube d} {j n : ℕ} (u : Vec d → ℝ) (hR : R ∈ descendantsAtDepth Q j) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : cubeAverage R (cubeProjection Q (j + n) u) = cubeAverage R u

theorem HCPolySupport.cubeScaleFactor_eq_div_pow_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) : cubeScaleFactor R = cubeScaleFactor Q / 3 ^ j

theorem HCPolySupport.cubeBesovScaleWeight_eq_mul_rpow_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (s : ℝ) (hR : R ∈ descendantsAtDepth Q j) : cubeBesovScaleWeight s R = cubeBesovScaleWeight s Q * Real.rpow 3 (s * ↑j)

Besov scale weights on a depth-j descendant differ from the parent weight by the triadic factor 3^(s j).

theorem HCPolySupport.cubeBesovScaleWeight_neg_parent_mul_rpow_eq_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (r : ℝ) (hR : R ∈ descendantsAtDepth Q j) : cubeBesovScaleWeight (-r) Q * Real.rpow 3 (-r * ↑j) = cubeBesovScaleWeight (-r) R

Parent-weight form of the descendant Besov-weight identity. For a depth-j descendant, the parent scale weight times the triadic depth factor is the descendant scale weight.

theorem HCPolySupport.cubeBesovScaleWeight_neg_mul_rpow_eq_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (r : ℝ) (hR : R ∈ descendantsAtDepth Q j) : cubeBesovScaleWeight (-r) R * Real.rpow 3 (r * ↑j) = cubeBesovScaleWeight (-r) Q

Cancellation form of the descendant Besov-weight identity used in the small-cube Caccioppoli summation.

theorem HCPolySupport.cubeBesovCircDepthAverage_add_eq_descendantsAverage_cubeBesovCircDepthAverage {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (j n : ℕ) : cubeBesovCircDepthAverage Q p u (j + n) = descendantsAverage Q j fun (R : TriadicCube d) => cubeBesovCircDepthAverage R p u n

theorem HCPolySupport.cubeBesovCircDepthAverage_projection_eventually_constant {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (N r : ℕ) : cubeBesovCircDepthAverage Q 2 (cubeProjection Q (N + 1) u) (N + 1 + r) = cubeBesovCircDepthAverage Q 2 (cubeProjection Q (N + 1) u) (N + 1)

theorem HCPolySupport.cubeBesovCircDepthSeminorm_projection_eventually_geometric {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (N r : ℕ) : cubeBesovCircDepthSeminorm Q 1 2 (cubeProjection Q (N + 1) u) (N + 1 + r) = (1 / 3) ^ r * cubeBesovCircDepthSeminorm Q 1 2 (cubeProjection Q (N + 1) u) (N + 1)

theorem HCPolySupport.cubeBesovCircDepthAverage_projection_eq_of_le {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (N j : ℕ) (hj : j ≤ N + 1) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : cubeBesovCircDepthAverage Q 2 (cubeProjection Q (N + 1) u) j = cubeBesovCircDepthAverage Q 2 u j

theorem HCPolySupport.cubeBesovCircDepthSeminorm_projection_eq_of_le {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (s : ℝ) (N j : ℕ) (hj : j ≤ N + 1) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : cubeBesovCircDepthSeminorm Q s 2 (cubeProjection Q (N + 1) u) j = cubeBesovCircDepthSeminorm Q s 2 u j

theorem HCPolySupport.cubeBesovCircPartialNorm_projection_eq {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (N : ℕ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : cubeBesovCircPartialNorm Q 1 2 1 (N + 1) (cubeProjection Q (N + 1) u) = cubeBesovCircPartialNorm Q 1 2 1 (N + 1) u

@[simp]

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

theorem HCPolySupport.cubeBesovCircPartialNorm_one_mono {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) {M N : ℕ} (hMN : M ≤ N) : cubeBesovCircPartialNorm Q s p 1 M u ≤ cubeBesovCircPartialNorm Q s p 1 N u

theorem HCPolySupport.cubeBesovCircPartialNorm_one_depth_zero_eq_scaleWeight_neg_mul_norm_cubeAverage {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) : cubeBesovCircPartialNorm Q s p 1 0 u = cubeBesovScaleWeight (-s) Q * ‖cubeAverage Q u‖

theorem HCPolySupport.cubeLpNorm_projection_depth_zero_eq_norm_cubeAverage {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (hp0 : p ≠ 0) : cubeLpNorm Q p (cubeProjection Q 0 u) = ‖cubeAverage Q u‖

theorem HCPolySupport.cubeBesovCircNorm_projection_zero_le_three_halves_mul_cubeBesovCircPartialNorm_zero_of_memLp {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) : cubeBesovCircNorm Q 1 2 1 (cubeProjection Q 0 u) ≤ 3 / 2 * cubeBesovCircPartialNorm Q 1 2 1 0 u

theorem HCPolySupport.cubeBesovCircNorm_projection_succ_le_three_halves_mul_cubeBesovCircPartialNorm_of_memLp {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (N : ℕ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : cubeBesovCircNorm Q 1 2 1 (cubeProjection Q (N + 1) u) ≤ 3 / 2 * cubeBesovCircPartialNorm Q 1 2 1 (N + 1) u

theorem HCPolySupport.circNorm_projection_succ_le_three_halves_mul_circPartialNorm_on_descendants {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (M : ℕ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (j : ℕ) : j ∈ Finset.range (M + 1) → ∀ R ∈ descendantsAtDepth Q j, cubeBesovCircNorm R 1 2 1 (cubeProjection R (M - j + 1) u) ≤ 3 / 2 * cubeBesovCircPartialNorm R 1 2 1 (M - j + 1) u

theorem HCPolySupport.cubeBesovCircNorm_projection_le_three_halves_mul_cubeBesovCircPartialNorm_of_memLp {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (M : ℕ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : cubeBesovCircNorm Q 1 2 1 (cubeProjection Q M u) ≤ 3 / 2 * cubeBesovCircPartialNorm Q 1 2 1 M u

theorem HCPolySupport.cubeBesovCircNorm_projection_le_threeHalves_partial_onDescendants {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (M : ℕ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (j : ℕ) : j ∈ Finset.range (M + 1) → ∀ R ∈ descendantsAtDepth Q j, cubeBesovCircNorm R 1 2 1 (cubeProjection R (M - j) u) ≤ 3 / 2 * cubeBesovCircPartialNorm R 1 2 1 (M - j) u