Coarse-graining support: Support.Besov.Negative.ExactCirc

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

Exact concrete circ negative Besov kernel

This is the extended-valued source-facing circ lane from Chapter 1. Its natural depth j represents the manuscript scale n = Q.scale - j, and its blocks are exactly the disjoint descendants at that depth.

def HCPolySupport.ExactCircFiniteAdmissible (s p q : ℝ) : Prop

Admissible finite-q circ parameters. The real exponents are finite by construction; the final implication is the source restriction at s = 1.

Equations

• HCPolySupport.ExactCircFiniteAdmissible s p q = (0 < s ∧ s ≤ 1 ∧ 1 ≤ p ∧ 1 ≤ q ∧ (s = 1 → q = 1))

def HCPolySupport.ExactCircTopAdmissible (s p : ℝ) : Prop

Admissible q = ∞ circ parameters.

Equations

• HCPolySupport.ExactCircTopAdmissible s p = (0 < s ∧ s < 1 ∧ 1 ≤ p)

structure HCPolySupport.ExactCircFiniteParameters : Type

Finite-q parameters for the exact concrete circ seminorm.

• s : ℝ

  Negative smoothness exponent.

• p : ℝ

  Data integrability exponent.

• q : ℝ

  Finite aggregation exponent.

• admissible : ExactCircFiniteAdmissible self.s self.p self.q

structure HCPolySupport.ExactCircTopParameters : Type

q = ∞ parameters for the exact concrete circ seminorm.

• s : ℝ

  Negative smoothness exponent.

• p : ℝ

  Data integrability exponent.

• admissible : ExactCircTopAdmissible self.s self.p

theorem HCPolySupport.ExactCircFiniteParameters.s_pos (P : ExactCircFiniteParameters) : 0 < P.s

theorem HCPolySupport.ExactCircFiniteParameters.s_le_one (P : ExactCircFiniteParameters) : P.s ≤ 1

theorem HCPolySupport.ExactCircFiniteParameters.p_one_le (P : ExactCircFiniteParameters) : 1 ≤ P.p

theorem HCPolySupport.ExactCircFiniteParameters.q_one_le (P : ExactCircFiniteParameters) : 1 ≤ P.q

theorem HCPolySupport.ExactCircFiniteParameters.q_eq_one_of_s_eq_one (P : ExactCircFiniteParameters) (hs : P.s = 1) : P.q = 1

noncomputable def HCPolySupport.ExactCircFiniteParameters.pExponent (P : ExactCircFiniteParameters) : ENNReal

The finite real p exponent as an ENNReal exponent.

Equations

• P.pExponent = ENNReal.ofReal P.p

noncomputable def HCPolySupport.ExactCircFiniteParameters.qExponent (P : ExactCircFiniteParameters) : ENNReal

The finite real q exponent as an ENNReal exponent.

Equations

• P.qExponent = ENNReal.ofReal P.q

theorem HCPolySupport.ExactCircFiniteParameters.pExponent_ne_top (P : ExactCircFiniteParameters) : P.pExponent ≠ ⊤

theorem HCPolySupport.ExactCircFiniteParameters.qExponent_ne_top (P : ExactCircFiniteParameters) : P.qExponent ≠ ⊤

theorem HCPolySupport.ExactCircTopParameters.s_pos (P : ExactCircTopParameters) : 0 < P.s

theorem HCPolySupport.ExactCircTopParameters.s_lt_one (P : ExactCircTopParameters) : P.s < 1

theorem HCPolySupport.ExactCircTopParameters.p_one_le (P : ExactCircTopParameters) : 1 ≤ P.p

noncomputable def HCPolySupport.ExactCircTopParameters.pExponent (P : ExactCircTopParameters) : ENNReal

The finite real p exponent as an ENNReal exponent.

Equations

• P.pExponent = ENNReal.ofReal P.p

theorem HCPolySupport.ExactCircTopParameters.pExponent_ne_top (P : ExactCircTopParameters) : P.pExponent ≠ ⊤

structure HCPolySupport.ExactCircIntegrable {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) : Prop

Integrability certificates for the normalized averages on every disjoint block used by the source circ seminorm.

• block (j : ℕ) (R : TriadicCube d) : R ∈ descendantsAtDepth Q j → MeasureTheory.Integrable f (normalizedCubeMeasure R)

theorem HCPolySupport.exactCircZeroIntegrable {d : ℕ} (Q : TriadicCube d) : ExactCircIntegrable Q fun (x : Vec d) => 0

Canonical block-integrability data for the zero function.

def HCPolySupport.exactCircSourceDepth {d : ℕ} (Q : TriadicCube d) (j : ℕ) : ℤ

The manuscript source index represented by a natural descendant depth.

Equations

• HCPolySupport.exactCircSourceDepth Q j = Q.scale - ↑j

theorem HCPolySupport.exactCircSourceDepth_eq {d : ℕ} (Q : TriadicCube d) (j : ℕ) : exactCircSourceDepth Q j = Q.scale - ↑j

theorem HCPolySupport.exactCircSourceDepth_le_scale {d : ℕ} (Q : TriadicCube d) (j : ℕ) : exactCircSourceDepth Q j ≤ Q.scale

theorem HCPolySupport.exists_exactCircDepth_of_le_scale {d : ℕ} (Q : TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) : ∃ (j : ℕ), exactCircSourceDepth Q j = n

theorem HCPolySupport.exactCirc_descendant_scale {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) : R.scale = exactCircSourceDepth Q j

A depth-j descendant has exactly the source scale n = Q.scale - j.

theorem HCPolySupport.exactCircDescendants_nonempty {d : ℕ} (Q : TriadicCube d) (j : ℕ) : (descendantsAtDepth Q j).Nonempty

noncomputable def HCPolySupport.exactCircBlockMean {d : ℕ} (R : TriadicCube d) (f : Vec d → ℝ) (_hf : MeasureTheory.Integrable f (normalizedCubeMeasure R)) : ℝ

The normalized ordinary-cube average on a disjoint circ block.

Equations

• HCPolySupport.exactCircBlockMean R f _hf = ∫ (x : HCPolySupport.Vec d), f x ∂HCPolySupport.normalizedCubeMeasure R

noncomputable def HCPolySupport.exactCircDepthWeight {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) : ENNReal

The exact source weight 3^(n s) at descendant depth j.

Equations

• HCPolySupport.exactCircDepthWeight Q s j = 3 ^ (↑(HCPolySupport.exactCircSourceDepth Q j) * s)

noncomputable def HCPolySupport.exactCircDepthAverage {d : ℕ} (Q : TriadicCube d) (p : ℝ) (f : Vec d → ℝ) (hf : ExactCircIntegrable Q f) (j : ℕ) : ENNReal

The exact normalized finite ℓ^p average of the absolute block means.

Equations

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

noncomputable def HCPolySupport.exactCircDepthTerm {d : ℕ} (Q : TriadicCube d) (s p : ℝ) (f : Vec d → ℝ) (hf : ExactCircIntegrable Q f) (j : ℕ) : ENNReal

The weighted source depth term of the concrete circ seminorm.

Equations

• HCPolySupport.exactCircDepthTerm Q s p f hf j = HCPolySupport.exactCircDepthWeight Q s j * HCPolySupport.exactCircDepthAverage Q p f hf j ^ p⁻¹

noncomputable def HCPolySupport.exactCircFiniteSeminorm {d : ℕ} (P : ExactCircFiniteParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : ExactCircIntegrable Q f) : ENNReal

The exact finite-q concrete circ negative Besov seminorm.

Equations

• HCPolySupport.exactCircFiniteSeminorm P Q f hf = (∑' (j : ℕ), HCPolySupport.exactCircDepthTerm Q P.s P.p f hf j ^ P.q) ^ P.q⁻¹

noncomputable def HCPolySupport.exactCircTopSeminorm {d : ℕ} (P : ExactCircTopParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : ExactCircIntegrable Q f) : ENNReal

The exact q = ∞ concrete circ negative Besov seminorm.

Equations

• HCPolySupport.exactCircTopSeminorm P Q f hf = ⨆ (j : ℕ), HCPolySupport.exactCircDepthTerm Q P.s P.p f hf j

theorem HCPolySupport.exactCircBlockMean_eq {d : ℕ} (R : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.Integrable f (normalizedCubeMeasure R)) : exactCircBlockMean R f hf = ∫ (x : Vec d), f x ∂normalizedCubeMeasure R

Evaluation of the certified normalized disjoint block mean.

theorem HCPolySupport.exactCircBlockMean_zero {d : ℕ} (R : TriadicCube d) (hf : MeasureTheory.Integrable (fun (x : Vec d) => 0) (normalizedCubeMeasure R)) : exactCircBlockMean R (fun (x : Vec d) => 0) hf = 0

theorem HCPolySupport.exactCircBlockMean_congr_ae {d : ℕ} (R : TriadicCube d) {f g : Vec d → ℝ} (hf : MeasureTheory.Integrable f (normalizedCubeMeasure R)) (hg : MeasureTheory.Integrable g (normalizedCubeMeasure R)) (hfg : f =ᵐ[normalizedCubeMeasure R] g) : exactCircBlockMean R f hf = exactCircBlockMean R g hg

theorem HCPolySupport.exactCircDepthAverage_congr_ae {d : ℕ} (Q : TriadicCube d) (p : ℝ) {f g : Vec d → ℝ} (hf : ExactCircIntegrable Q f) (hg : ExactCircIntegrable Q g) (hfg : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, f =ᵐ[normalizedCubeMeasure R] g) (j : ℕ) : exactCircDepthAverage Q p f hf j = exactCircDepthAverage Q p g hg j

A normalized disjoint-block depth average depends only on the a.e. representatives on each ordinary descendant block.

theorem HCPolySupport.exactCircDepthTerm_congr_ae {d : ℕ} (Q : TriadicCube d) (s p : ℝ) {f g : Vec d → ℝ} (hf : ExactCircIntegrable Q f) (hg : ExactCircIntegrable Q g) (hfg : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, f =ᵐ[normalizedCubeMeasure R] g) (j : ℕ) : exactCircDepthTerm Q s p f hf j = exactCircDepthTerm Q s p g hg j

A weighted circ depth term depends only on the a.e. representatives on each ordinary descendant block.

theorem HCPolySupport.exactCircFiniteSeminorm_congr_ae {d : ℕ} (P : ExactCircFiniteParameters) (Q : TriadicCube d) {f g : Vec d → ℝ} (hf : ExactCircIntegrable Q f) (hg : ExactCircIntegrable Q g) (hfg : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, f =ᵐ[normalizedCubeMeasure R] g) : exactCircFiniteSeminorm P Q f hf = exactCircFiniteSeminorm P Q g hg

The finite-q exact circ seminorm depends only on the a.e. representatives on every ordinary descendant block.

theorem HCPolySupport.exactCircTopSeminorm_congr_ae {d : ℕ} (P : ExactCircTopParameters) (Q : TriadicCube d) {f g : Vec d → ℝ} (hf : ExactCircIntegrable Q f) (hg : ExactCircIntegrable Q g) (hfg : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, f =ᵐ[normalizedCubeMeasure R] g) : exactCircTopSeminorm P Q f hf = exactCircTopSeminorm P Q g hg

The q = ∞ exact circ seminorm depends only on the a.e. representatives on every ordinary descendant block.

theorem HCPolySupport.exactCircFiniteDepthAverage_zero {d : ℕ} (P : ExactCircFiniteParameters) (Q : TriadicCube d) (j : ℕ) : exactCircDepthAverage Q P.p (fun (x : Vec d) => 0) ⋯ j = 0

The depth average vanishes for zero data at every admissible finite-q exponent.

theorem HCPolySupport.exactCircTopDepthAverage_zero {d : ℕ} (P : ExactCircTopParameters) (Q : TriadicCube d) (j : ℕ) : exactCircDepthAverage Q P.p (fun (x : Vec d) => 0) ⋯ j = 0

The depth average vanishes for zero data at every admissible q = ∞ exponent.

theorem HCPolySupport.exactCircFiniteDepthTerm_zero {d : ℕ} (P : ExactCircFiniteParameters) (Q : TriadicCube d) (j : ℕ) : exactCircDepthTerm Q P.s P.p (fun (x : Vec d) => 0) ⋯ j = 0

The weighted depth term vanishes for zero data at every admissible finite-q exponent.

theorem HCPolySupport.exactCircTopDepthTerm_zero {d : ℕ} (P : ExactCircTopParameters) (Q : TriadicCube d) (j : ℕ) : exactCircDepthTerm Q P.s P.p (fun (x : Vec d) => 0) ⋯ j = 0

The weighted depth term vanishes for zero data at every admissible q = ∞ exponent.

theorem HCPolySupport.exactCircDepthAverage_eq {d : ℕ} (Q : TriadicCube d) (p : ℝ) (f : Vec d → ℝ) (hf : ExactCircIntegrable Q f) (j : ℕ) : exactCircDepthAverage Q p f hf j = (↑(descendantsAtDepth Q j).card)⁻¹ * ∑ R ∈ (descendantsAtDepth Q j).attach, ENNReal.ofReal |exactCircBlockMean (↑R) f ⋯| ^ p

Evaluation of the finite normalized disjoint block average.

theorem HCPolySupport.exactCircDepthTerm_eq {d : ℕ} (Q : TriadicCube d) (s p : ℝ) (f : Vec d → ℝ) (hf : ExactCircIntegrable Q f) (j : ℕ) : exactCircDepthTerm Q s p f hf j = exactCircDepthWeight Q s j * exactCircDepthAverage Q p f hf j ^ p⁻¹

Evaluation of the weighted concrete circ depth term.

theorem HCPolySupport.exactCircFiniteSeminorm_eq {d : ℕ} (P : ExactCircFiniteParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : ExactCircIntegrable Q f) : exactCircFiniteSeminorm P Q f hf = (∑' (j : ℕ), exactCircDepthTerm Q P.s P.p f hf j ^ P.q) ^ P.q⁻¹

Evaluation of the infinite finite-q aggregation.

theorem HCPolySupport.exactCircTopSeminorm_eq {d : ℕ} (P : ExactCircTopParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : ExactCircIntegrable Q f) : exactCircTopSeminorm P Q f hf = ⨆ (j : ℕ), exactCircDepthTerm Q P.s P.p f hf j

Evaluation of the q = ∞ aggregation.

theorem HCPolySupport.exactCircFiniteSeminorm_zero {d : ℕ} (P : ExactCircFiniteParameters) (Q : TriadicCube d) : exactCircFiniteSeminorm P Q (fun (x : Vec d) => 0) ⋯ = 0

The exact finite-q circ seminorm vanishes on the zero function.

theorem HCPolySupport.exactCircTopSeminorm_zero {d : ℕ} (P : ExactCircTopParameters) (Q : TriadicCube d) : exactCircTopSeminorm P Q (fun (x : Vec d) => 0) ⋯ = 0

The exact q = ∞ circ seminorm vanishes on the zero function.

theorem HCPolySupport.exactCircDepthAverage_nonneg {d : ℕ} (Q : TriadicCube d) (p : ℝ) (f : Vec d → ℝ) (hf : ExactCircIntegrable Q f) (j : ℕ) : 0 ≤ exactCircDepthAverage Q p f hf j

All extended values in the exact concrete circ kernel are nonnegative.

theorem HCPolySupport.exactCircFiniteSeminorm_nonneg {d : ℕ} (P : ExactCircFiniteParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : ExactCircIntegrable Q f) : 0 ≤ exactCircFiniteSeminorm P Q f hf

theorem HCPolySupport.exactCircTopSeminorm_nonneg {d : ℕ} (P : ExactCircTopParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : ExactCircIntegrable Q f) : 0 ≤ exactCircTopSeminorm P Q f hf