Coarse-graining support: Support.Besov.ProjectionCharacterization

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

Local projection-characterization lemmas for the positive cube Besov package.

This first checkpoint stays deliberately depth-local. It identifies the oscillation on each descendant cube with the local projection error against cubeProjection Q j, then packages the resulting depth-average and depth-seminorm reformulations. It also records the analogous local cubeIncrement identity on descendants one generation deeper.

noncomputable def HCPolySupport.cubeProjectionResidual {d : ℕ} (Q : TriadicCube d) (j : ℕ) (u : Vec d → ℝ) : Vec d → ℝ

The pointwise error of u relative to its cube projection at depth j.

Equations

• HCPolySupport.cubeProjectionResidual Q j u x = u x - HCPolySupport.cubeProjection Q j u x

noncomputable def HCPolySupport.cubeProjectionGap {d : ℕ} (Q : TriadicCube d) (j n : ℕ) (u : Vec d → ℝ) : Vec d → ℝ

The difference between the cube projections of u at depths j + n and j.

Equations

• HCPolySupport.cubeProjectionGap Q j n u x = HCPolySupport.cubeProjection Q (j + n) u x - HCPolySupport.cubeProjection Q j u x

@[simp]

theorem HCPolySupport.cubeProjectionResidual_apply {d : ℕ} (Q : TriadicCube d) (j : ℕ) (u : Vec d → ℝ) (x : Vec d) : cubeProjectionResidual Q j u x = u x - cubeProjection Q j u x

@[simp]

theorem HCPolySupport.cubeProjectionGap_apply {d : ℕ} (Q : TriadicCube d) (j n : ℕ) (u : Vec d → ℝ) (x : Vec d) : cubeProjectionGap Q j n u x = cubeProjection Q (j + n) u x - cubeProjection Q j u x

theorem HCPolySupport.cubeFluctuation_ae_eq_sub_cubeProjection_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (u : Vec d → ℝ) (hR : R ∈ descendantsAtDepth Q j) : cubeFluctuation R u =ᵐ[normalizedCubeMeasure R] fun (x : Vec d) => u x - cubeProjection Q j u x

theorem HCPolySupport.cubeFluctuation_ae_eq_cubeProjectionResidual_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (u : Vec d → ℝ) (hR : R ∈ descendantsAtDepth Q j) : cubeFluctuation R u =ᵐ[normalizedCubeMeasure R] cubeProjectionResidual Q j u

theorem HCPolySupport.cubeBesovOscillation_eq_cubeLpNorm_sub_cubeProjection_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (p : ENNReal) (u : Vec d → ℝ) (hR : R ∈ descendantsAtDepth Q j) : cubeBesovOscillation R p u = cubeLpNorm R p fun (x : Vec d) => u x - cubeProjection Q j u x

theorem HCPolySupport.cubeBesovOscillation_eq_cubeLpNorm_cubeProjectionResidual_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (p : ENNReal) (u : Vec d → ℝ) (hR : R ∈ descendantsAtDepth Q j) : cubeBesovOscillation R p u = cubeLpNorm R p (cubeProjectionResidual Q j u)

theorem HCPolySupport.cubeBesovDepthAverage_eq_descendantsAverage_projection_error {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (j : ℕ) : cubeBesovDepthAverage Q p u j = descendantsAverage Q j fun (R : TriadicCube d) => (cubeLpNorm R p fun (x : Vec d) => u x - cubeProjection Q j u x) ^ p.toReal

theorem HCPolySupport.cubeBesovDepthAverage_eq_descendantsAverage_projectionResidual {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (j : ℕ) : cubeBesovDepthAverage Q p u j = descendantsAverage Q j fun (R : TriadicCube d) => cubeLpNorm R p (cubeProjectionResidual Q j u) ^ p.toReal

theorem HCPolySupport.cubeBesovDepthSeminorm_eq_projection_error {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (j : ℕ) : cubeBesovDepthSeminorm Q s p u j = cubeBesovDepthWeight Q s j * (descendantsAverage Q j fun (R : TriadicCube d) => (cubeLpNorm R p fun (x : Vec d) => u x - cubeProjection Q j u x) ^ p.toReal) ^ (1 / p.toReal)

theorem HCPolySupport.cubeBesovDepthSeminorm_eq_projectionResidual {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (j : ℕ) : cubeBesovDepthSeminorm Q s p u j = cubeBesovDepthWeight Q s j * (descendantsAverage Q j fun (R : TriadicCube d) => cubeLpNorm R p (cubeProjectionResidual Q j u) ^ p.toReal) ^ (1 / p.toReal)

theorem HCPolySupport.cubeBesovPartialSeminorm_eq_projection_error {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) : cubeBesovPartialSeminorm Q s p q N u = (∑ j ∈ Finset.range (N + 1), (cubeBesovDepthWeight Q s j * (descendantsAverage Q j fun (R : TriadicCube d) => (cubeLpNorm R p fun (x : Vec d) => u x - cubeProjection Q j u x) ^ p.toReal) ^ (1 / p.toReal)) ^ q.toReal) ^ (1 / q.toReal)

theorem HCPolySupport.cubeBesovPartialNorm_eq_projection_error {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) : cubeBesovPartialNorm Q s p q N u = (∑ j ∈ Finset.range (N + 1), (cubeBesovDepthWeight Q s j * (descendantsAverage Q j fun (R : TriadicCube d) => (cubeLpNorm R p fun (x : Vec d) => u x - cubeProjection Q j u x) ^ p.toReal) ^ (1 / p.toReal)) ^ q.toReal) ^ (1 / q.toReal) + cubeBesovScaleWeight s Q * ‖cubeAverage Q u‖

theorem HCPolySupport.sum_cubeIncrement_eq_cubeProjectionGap {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (j n : ℕ) : (fun (x : Vec d) => ∑ m ∈ Finset.range n, cubeIncrement Q (j + m + 1) u x) = cubeProjectionGap Q j n u

theorem HCPolySupport.cubeLpNorm_sum_cubeIncrement_eq_cubeProjectionGap {d : ℕ} (S Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (j n : ℕ) : (cubeLpNorm S p fun (x : Vec d) => ∑ m ∈ Finset.range n, cubeIncrement Q (j + m + 1) u x) = cubeLpNorm S p (cubeProjectionGap Q j n u)

theorem HCPolySupport.cubeBesovDepthAverage_depth_zero_eq_sub_cubeProjection {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) : cubeBesovDepthAverage Q p u 0 = (cubeLpNorm Q p fun (x : Vec d) => u x - cubeProjection Q 0 u x) ^ p.toReal

theorem HCPolySupport.cubeBesovDepthAverage_depth_zero_eq_sub_cubeIncrement {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) : cubeBesovDepthAverage Q p u 0 = (cubeLpNorm Q p fun (x : Vec d) => u x - cubeIncrement Q 0 u x) ^ p.toReal

theorem HCPolySupport.cubeIncrement_ae_eq_sub_cubeProjection_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (u : Vec d → ℝ) (hR : R ∈ descendantsAtDepth Q (j + 1)) : cubeIncrement Q (j + 1) u =ᵐ[normalizedCubeMeasure R] fun (x : Vec d) => cubeAverage R u - cubeProjection Q j u x

theorem HCPolySupport.cubeLpNorm_cubeIncrement_eq_sub_cubeProjection_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (p : ENNReal) (u : Vec d → ℝ) (hR : R ∈ descendantsAtDepth Q (j + 1)) : cubeLpNorm R p (cubeIncrement Q (j + 1) u) = cubeLpNorm R p fun (x : Vec d) => cubeAverage R u - cubeProjection Q j u x

theorem HCPolySupport.cubeProjectionGap_ae_eq_sub_cubeProjection_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} (u : Vec d → ℝ) {j n : ℕ} (hR : R ∈ descendantsAtDepth Q (j + n)) : cubeProjectionGap Q j n u =ᵐ[normalizedCubeMeasure R] fun (x : Vec d) => cubeAverage R u - cubeProjection Q j u x

theorem HCPolySupport.cubeLpNorm_cubeProjectionGap_eq_sub_cubeProjection_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} (p : ENNReal) (u : Vec d → ℝ) {j n : ℕ} (hR : R ∈ descendantsAtDepth Q (j + n)) : cubeLpNorm R p (cubeProjectionGap Q j n u) = cubeLpNorm R p fun (x : Vec d) => cubeAverage R u - cubeProjection Q j u x

theorem HCPolySupport.sum_cubeIncrement_ae_eq_sub_cubeProjection_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} (u : Vec d → ℝ) {j n : ℕ} (hR : R ∈ descendantsAtDepth Q (j + n)) : (fun (x : Vec d) => ∑ m ∈ Finset.range n, cubeIncrement Q (j + m + 1) u x) =ᵐ[normalizedCubeMeasure R] fun (x : Vec d) => cubeAverage R u - cubeProjection Q j u x

theorem HCPolySupport.cubeLpNorm_sum_cubeIncrement_eq_sub_cubeProjection_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} (p : ENNReal) (u : Vec d → ℝ) {j n : ℕ} (hR : R ∈ descendantsAtDepth Q (j + n)) : (cubeLpNorm R p fun (x : Vec d) => ∑ m ∈ Finset.range n, cubeIncrement Q (j + m + 1) u x) = cubeLpNorm R p fun (x : Vec d) => cubeAverage R u - cubeProjection Q j u x