Coarse-graining support: Support.Book.Ch01.Definitions

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

Chapter 1 public vocabulary

This file gives Chapter 1 a note-facing entry point without redefining the underlying analysis. The unqualified names expose the exact proof-carrying normalized and Besov kernels. Earlier totalized and disjoint-cube conventions are retained only in Book.Ch01.Legacy.

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.Vec (d : ℕ) : Type

The ambient coordinate space used throughout Chapter 1.

Equations

• HCPolySupport.Book.Ch01.Vec d = HCPolySupport.Vec d

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.Cube (d : ℕ) : Type

The translated triadic cubes used throughout Chapter 1.

Equations

• HCPolySupport.Book.Ch01.Cube d = HCPolySupport.TriadicCube d

Exact normalized cube quantities

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.normalizedAverage {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : Cube d) (f : Vec d → E) (hf : MeasureTheory.Integrable f (cubeBoundedMeasurableDomain Q).restrictedVolume) : E

The proof-carrying normalized Bochner average on a triadic cube.

Equations

• HCPolySupport.Book.Ch01.normalizedAverage Q f hf = (HCPolySupport.cubeBoundedMeasurableDomain Q).average f hf

theorem HCPolySupport.Book.Ch01.normalizedAverage_eq_volume_toReal_inv_smul_setIntegral {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : Cube d) (f : Vec d → E) (hf : MeasureTheory.Integrable f (cubeBoundedMeasurableDomain Q).restrictedVolume) : normalizedAverage Q f hf = (MeasureTheory.volume (cubeSet Q)).toReal⁻¹ • ∫ (x : HCPolySupport.Vec d) in cubeSet Q, f x

The exact set-integral formula for the normalized Bochner cube average.

theorem HCPolySupport.Book.Ch01.normalizedAverage_eq_cubeAverage {d : ℕ} (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.Integrable f (cubeBoundedMeasurableDomain Q).restrictedVolume) : normalizedAverage Q f hf = cubeAverage Q f

For scalar functions, the proof-carrying average is the established cube average.

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.normalizedLpENorm {d : ℕ} {E : Type u_1} [ENorm E] [TopologicalSpace E] (Q : Cube d) (p : ENNReal) (f : Vec d → E) : ENNReal

The extended normalized cube L^p value.

Equations

• HCPolySupport.Book.Ch01.normalizedLpENorm Q p f = (HCPolySupport.cubeBoundedMeasurableDomain Q).normalizedLpENorm p f

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.normalizedLpNorm {d : ℕ} {E : Type u_1} [TopologicalSpace E] [ContinuousENorm E] (Q : Cube d) (p : ENNReal) (f : Vec d → E) (hf : MeasureTheory.MemLp f p (cubeBoundedMeasurableDomain Q).normalizedVolume) : ℝ

The finite normalized cube L^p value certified by a MemLp witness.

Equations

• HCPolySupport.Book.Ch01.normalizedLpNorm Q p f hf = (HCPolySupport.cubeBoundedMeasurableDomain Q).normalizedLpNorm p f hf

theorem HCPolySupport.Book.Ch01.normalizedLpENorm_eq_eLpNorm_normalizedCubeMeasure {d : ℕ} {E : Type u_1} [ENorm E] [TopologicalSpace E] (Q : Cube d) (p : ENNReal) (f : Vec d → E) : normalizedLpENorm Q p f = MeasureTheory.eLpNorm f p (normalizedCubeMeasure Q)

The cube extended norm is eLpNorm for normalized cube measure.

theorem HCPolySupport.Book.Ch01.normalizedLpNorm_eq_integral_rpow {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : Cube d) (p : ENNReal) (hp_one : 1 ≤ p) (hp_top : p ≠ ⊤) (f : Vec d → E) (hf : MeasureTheory.MemLp f p (cubeBoundedMeasurableDomain Q).normalizedVolume) : normalizedLpNorm Q p f hf = (∫ (x : HCPolySupport.Vec d), ‖f x‖ ^ p.toReal ∂normalizedCubeMeasure Q) ^ p.toReal⁻¹

For finite p ≥ 1, the exact normalized cube norm has the manuscript moment formula.

theorem HCPolySupport.Book.Ch01.normalizedLpENorm_top_eq_essSup {d : ℕ} {E : Type u_1} [ENorm E] [TopologicalSpace E] (Q : Cube d) (f : Vec d → E) (hf : MeasureTheory.AEStronglyMeasurable f (normalizedCubeMeasure Q)) : normalizedLpENorm Q ⊤ f = essSup (fun (x : Vec d) => ‖f x‖ₑ) (normalizedCubeMeasure Q)

At p = ∞, the exact normalized cube value is the essential supremum.

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.normalizedEuclideanLpENorm {d n : ℕ} (Q : Cube d) (p : ENNReal) (f : Vec d → Vec n) : ENNReal

The extended normalized Euclidean L^p value of a vector field.

Equations

• HCPolySupport.Book.Ch01.normalizedEuclideanLpENorm Q p f = (HCPolySupport.cubeBoundedMeasurableDomain Q).normalizedEuclideanLpENorm p f

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.normalizedEuclideanLpNorm {d n : ℕ} (Q : Cube d) (p : ENNReal) (f : Vec d → Vec n) (hf : MeasureTheory.MemLp (fun (x : Vec d) => euclideanNorm (f x)) p (cubeBoundedMeasurableDomain Q).normalizedVolume) : ℝ

The finite normalized Euclidean L^p value certified by a MemLp witness.

Equations

• HCPolySupport.Book.Ch01.normalizedEuclideanLpNorm Q p f hf = (HCPolySupport.cubeBoundedMeasurableDomain Q).normalizedEuclideanLpNorm p f hf

theorem HCPolySupport.Book.Ch01.normalizedEuclideanLpNorm_eq_integral_rpow {d n : ℕ} (Q : Cube d) (p : ENNReal) (hp_one : 1 ≤ p) (hp_top : p ≠ ⊤) (f : Vec d → Vec n) (hf : MeasureTheory.MemLp (fun (x : Vec d) => euclideanNorm (f x)) p (cubeBoundedMeasurableDomain Q).normalizedVolume) : normalizedEuclideanLpNorm Q p f hf = (∫ (x : HCPolySupport.Vec d), euclideanNorm (f x) ^ p.toReal ∂normalizedCubeMeasure Q) ^ p.toReal⁻¹

For finite p ≥ 1, the vector lane uses explicit Euclidean magnitude.

theorem HCPolySupport.Book.Ch01.normalizedEuclideanLpENorm_top_eq_essSup {d n : ℕ} (Q : Cube d) (f : Vec d → Vec n) (hf : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => euclideanNorm (f x)) (normalizedCubeMeasure Q)) : normalizedEuclideanLpENorm Q ⊤ f = essSup (fun (x : Vec d) => ENNReal.ofReal (euclideanNorm (f x))) (normalizedCubeMeasure Q)

At p = ∞, the vector lane is the essential supremum of Euclidean magnitude.

Normalized Sobolev quantities

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.legacyCubeW1pSeminorm {d : ℕ} (Q : Cube d) (p : ENNReal) (Du : Vec d → Vec d) : ℝ

Legacy cube W^{1,p} seminorm with an arbitrary gradient representative. This is a cube-specialized compatibility alias, not the Chapter 1 weak-Sobolev carrier.

Equations

• HCPolySupport.Book.Ch01.legacyCubeW1pSeminorm Q p Du = HCPolySupport.cubeW1pSeminorm Q p Du

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.legacyCubeW1pNorm {d : ℕ} (Q : Cube d) (p : ENNReal) (u : Vec d → ℝ) (Du : Vec d → Vec d) : ℝ

Legacy cube W^{1,p} norm with an arbitrary gradient representative. This is a cube-specialized compatibility alias, not the Chapter 1 weak-Sobolev carrier.

Equations

• HCPolySupport.Book.Ch01.legacyCubeW1pNorm Q p u Du = HCPolySupport.cubeW1pNorm Q p u Du

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.normalizedW1pSeminorm {d : ℕ} (U : Set (Vec d)) (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 ≤ p) (hp_top : p ≠ ⊤) (u : W1pFunction U p) : ℝ

The Chapter 1 finite-exponent normalized W^{1,p} seminorm on a genuine weak-Sobolev witness over a nonempty bounded open convex domain.

Equations

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

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.normalizedW1pNorm {d : ℕ} (U : Set (Vec d)) (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 ≤ p) (hp_top : p ≠ ⊤) (u : W1pFunction U p) : ℝ

The Chapter 1 finite-exponent normalized W^{1,p} norm on a genuine weak-Sobolev witness over a nonempty bounded open convex domain.

Equations

• HCPolySupport.Book.Ch01.normalizedW1pNorm U hU hne p hp_one hp_top u = HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.norm (hU.toBoundedMeasurableDomain hne) p hp_one hp_top u

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.normalizedW1pSeminormTop {d : ℕ} (U : Set (Vec d)) (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (u : W1pFunction U ⊤) : ℝ

The Chapter 1 normalized W^{1,∞} seminorm on a genuine weak-Sobolev witness over a nonempty bounded open convex domain.

Equations

• HCPolySupport.Book.Ch01.normalizedW1pSeminormTop U hU hne u = HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.seminormTop (hU.toBoundedMeasurableDomain hne) u

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.normalizedW1pNormTop {d : ℕ} (U : Set (Vec d)) (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (u : W1pFunction U ⊤) : ℝ

The Chapter 1 normalized W^{1,∞} norm on a genuine weak-Sobolev witness, over a nonempty bounded open convex domain, using the manuscript's additive endpoint formula.

Equations

• HCPolySupport.Book.Ch01.normalizedW1pNormTop U hU hne u = HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.normTop (hU.toBoundedMeasurableDomain hne) u

Exact negative Sobolev quantities

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.normalizedZeroBoundaryWMinusOneSeminorm {d : ℕ} (U : Set (Vec d)) (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (hU.toBoundedMeasurableDomain hne).normalizedVolume) : ENNReal

The normalized zero-boundary W^{-1,p'} seminorm on U, with p the positive test exponent. Its test class is literal smooth compact support.

Equations

• HCPolySupport.Book.Ch01.normalizedZeroBoundaryWMinusOneSeminorm U hU hne p hp_one hp_top f hf = HCPolySupport.NegativeSobolev.smoothNegativeSobolevSeminorm hU hne p hp_one hp_top f hf

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.normalizedMeanZeroWMinusOneSeminorm {d : ℕ} (U : Set (Vec d)) (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (hU.toBoundedMeasurableDomain hne).normalizedVolume) : ENNReal

The normalized mean-zero W^{-1,p'} seminorm on U, with p the positive test exponent. Its test class consists of genuine mean-zero weak W^{1,p} witnesses.

Equations

• HCPolySupport.Book.Ch01.normalizedMeanZeroWMinusOneSeminorm U hU hne p hp_one hp_top f hf = HCPolySupport.NegativeSobolev.meanZeroNegativeSobolevSeminorm hU hne p hp_one hp_top f hf

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.normalizedZeroBoundaryHMinusOneSeminorm {d : ℕ} (U : Set (Vec d)) (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.conjExponent 2) (hU.toBoundedMeasurableDomain hne).normalizedVolume) : ENNReal

The zero-boundary normalized H^{-1} seminorm on U; this is the p = 2 instance with smooth compactly supported tests.

Equations

• HCPolySupport.Book.Ch01.normalizedZeroBoundaryHMinusOneSeminorm U hU hne f hf = HCPolySupport.NegativeSobolev.smoothNegativeHMinusOneSeminorm hU hne f hf

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.normalizedMeanZeroHMinusOneSeminorm {d : ℕ} (U : Set (Vec d)) (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.conjExponent 2) (hU.toBoundedMeasurableDomain hne).normalizedVolume) : ENNReal

The mean-zero normalized H^{-1} seminorm on U; this is the distinct p = 2 convention with genuine mean-zero weak W^{1,2} tests.

Equations

• HCPolySupport.Book.Ch01.normalizedMeanZeroHMinusOneSeminorm U hU hne f hf = HCPolySupport.NegativeSobolev.meanZeroNegativeHMinusOneSeminorm hU hne f hf

Exact positive overlap Besov quantities

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.PositiveBesovFiniteParameters : Type

Finite-q source parameters for the exact positive overlap Besov lane.

Equations

• HCPolySupport.Book.Ch01.PositiveBesovFiniteParameters = HCPolySupport.ExactOverlapFiniteParameters

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.PositiveBesovTopParameters : Type

q = ∞ source parameters for the exact positive overlap Besov lane.

Equations

• HCPolySupport.Book.Ch01.PositiveBesovTopParameters = HCPolySupport.ExactOverlapTopParameters

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.PositiveBesovIntegrable {d : ℕ} (Q : Cube d) (u : Vec d → ℝ) : Prop

Integrability witnesses for all averages in the exact positive Besov lane.

Equations

• HCPolySupport.Book.Ch01.PositiveBesovIntegrable Q u = HCPolySupport.ExactOverlapIntegrable Q u

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.positiveBesovFiniteSeminorm {d : ℕ} (P : PositiveBesovFiniteParameters) (Q : Cube d) (u : Vec d → ℝ) (hu : PositiveBesovIntegrable Q u) : ENNReal

The exact finite-q positive overlap Besov seminorm.

Equations

• HCPolySupport.Book.Ch01.positiveBesovFiniteSeminorm P Q u hu = HCPolySupport.exactOverlapFiniteSeminorm P Q u hu

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.positiveBesovFiniteNorm {d : ℕ} (P : PositiveBesovFiniteParameters) (Q : Cube d) (u : Vec d → ℝ) (hu : PositiveBesovIntegrable Q u) : ENNReal

The exact finite-q positive overlap Besov norm.

Equations

• HCPolySupport.Book.Ch01.positiveBesovFiniteNorm P Q u hu = HCPolySupport.exactOverlapFiniteNorm P Q u hu

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.positiveBesovTopSeminorm {d : ℕ} (P : PositiveBesovTopParameters) (Q : Cube d) (u : Vec d → ℝ) (hu : PositiveBesovIntegrable Q u) : ENNReal

The exact q = ∞ positive overlap Besov seminorm.

Equations

• HCPolySupport.Book.Ch01.positiveBesovTopSeminorm P Q u hu = HCPolySupport.exactOverlapTopSeminorm P Q u hu

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.positiveBesovTopNorm {d : ℕ} (P : PositiveBesovTopParameters) (Q : Cube d) (u : Vec d → ℝ) (hu : PositiveBesovIntegrable Q u) : ENNReal

The exact q = ∞ positive overlap Besov norm.

Equations

• HCPolySupport.Book.Ch01.positiveBesovTopNorm P Q u hu = HCPolySupport.exactOverlapTopNorm P Q u hu

theorem HCPolySupport.Book.Ch01.positiveBesovFiniteSeminorm_eq {d : ℕ} (P : PositiveBesovFiniteParameters) (Q : Cube d) (u : Vec d → ℝ) (hu : PositiveBesovIntegrable Q u) : positiveBesovFiniteSeminorm P Q u hu = (∑' (j : ℕ), exactOverlapDepthTerm Q P.s P.p u hu j ^ P.q) ^ P.q⁻¹

Formula for the exact finite-q positive overlap Besov seminorm.

theorem HCPolySupport.Book.Ch01.positiveBesovFiniteNorm_eq {d : ℕ} (P : PositiveBesovFiniteParameters) (Q : Cube d) (u : Vec d → ℝ) (hu : PositiveBesovIntegrable Q u) : positiveBesovFiniteNorm P Q u hu = positiveBesovFiniteSeminorm P Q u hu + exactOverlapRootWeight Q P.s * ENNReal.ofReal |exactOverlapRootMean Q u ⋯|

Formula for the exact finite-q positive overlap Besov norm.

theorem HCPolySupport.Book.Ch01.positiveBesovTopSeminorm_eq {d : ℕ} (P : PositiveBesovTopParameters) (Q : Cube d) (u : Vec d → ℝ) (hu : PositiveBesovIntegrable Q u) : positiveBesovTopSeminorm P Q u hu = ⨆ (j : ℕ), exactOverlapDepthTerm Q P.s P.p u hu j

Formula for the exact q = ∞ positive overlap Besov seminorm.

theorem HCPolySupport.Book.Ch01.positiveBesovTopNorm_eq {d : ℕ} (P : PositiveBesovTopParameters) (Q : Cube d) (u : Vec d → ℝ) (hu : PositiveBesovIntegrable Q u) : positiveBesovTopNorm P Q u hu = positiveBesovTopSeminorm P Q u hu + exactOverlapRootWeight Q P.s * ENNReal.ofReal |exactOverlapRootMean Q u ⋯|

Formula for the exact q = ∞ positive overlap Besov norm.

Exact dual negative Besov quantities

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.DualNegativeBesovQOneParameters : Type

Parameters for the exact negative q = 1 dual Besov lane.

Equations

• HCPolySupport.Book.Ch01.DualNegativeBesovQOneParameters = HCPolySupport.ExactDualQOneParameters

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.DualNegativeBesovFiniteParameters : Type

Parameters for the exact negative finite-interior dual Besov lane.

Equations

• HCPolySupport.Book.Ch01.DualNegativeBesovFiniteParameters = HCPolySupport.ExactDualFiniteParameters

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.DualNegativeBesovTopParameters : Type

Parameters for the exact negative q = ∞ dual Besov lane.

Equations

• HCPolySupport.Book.Ch01.DualNegativeBesovTopParameters = HCPolySupport.ExactDualTopParameters

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.DualNegativeBesovQOneFullTest {d : ℕ} (P : DualNegativeBesovQOneParameters) (Q : Cube d) : Type

Full test carrier for the exact negative q = 1 dual Besov norm.

Equations

• HCPolySupport.Book.Ch01.DualNegativeBesovQOneFullTest P Q = HCPolySupport.ExactDualQOneFullTest P Q

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.DualNegativeBesovQOneHattedTest {d : ℕ} (P : DualNegativeBesovQOneParameters) (Q : Cube d) : Type

Hatted test carrier for the exact negative q = 1 dual Besov seminorm.

Equations

• HCPolySupport.Book.Ch01.DualNegativeBesovQOneHattedTest P Q = HCPolySupport.ExactDualQOneHattedTest P Q

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.DualNegativeBesovFiniteFullTest {d : ℕ} (P : DualNegativeBesovFiniteParameters) (Q : Cube d) : Type

Full test carrier for the exact negative finite-interior dual Besov norm.

Equations

• HCPolySupport.Book.Ch01.DualNegativeBesovFiniteFullTest P Q = HCPolySupport.ExactDualFiniteFullTest P Q

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.DualNegativeBesovFiniteHattedTest {d : ℕ} (P : DualNegativeBesovFiniteParameters) (Q : Cube d) : Type

Hatted test carrier for the exact negative finite-interior dual Besov seminorm.

Equations

• HCPolySupport.Book.Ch01.DualNegativeBesovFiniteHattedTest P Q = HCPolySupport.ExactDualFiniteHattedTest P Q

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.DualNegativeBesovTopFullTest {d : ℕ} (P : DualNegativeBesovTopParameters) (Q : Cube d) : Type

Full test carrier for the exact negative q = ∞ dual Besov norm.

Equations

• HCPolySupport.Book.Ch01.DualNegativeBesovTopFullTest P Q = HCPolySupport.ExactDualTopFullTest P Q

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.DualNegativeBesovTopHattedTest {d : ℕ} (P : DualNegativeBesovTopParameters) (Q : Cube d) : Type

Hatted test carrier for the exact negative q = ∞ dual Besov seminorm.

Equations

• HCPolySupport.Book.Ch01.DualNegativeBesovTopHattedTest P Q = HCPolySupport.ExactDualTopHattedTest P Q

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.dualNegativeBesovQOneHattedSeminorm {d : ℕ} (P : DualNegativeBesovQOneParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : ENNReal

The exact negative q = 1 hatted dual Besov seminorm.

Equations

• HCPolySupport.Book.Ch01.dualNegativeBesovQOneHattedSeminorm P Q f hf = HCPolySupport.exactDualQOneHattedSeminorm P Q f hf

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.dualNegativeBesovQOneFullNorm {d : ℕ} (P : DualNegativeBesovQOneParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : ENNReal

The exact negative q = 1 full dual Besov norm.

Equations

• HCPolySupport.Book.Ch01.dualNegativeBesovQOneFullNorm P Q f hf = HCPolySupport.exactDualQOneFullNorm P Q f hf

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.dualNegativeBesovFiniteHattedSeminorm {d : ℕ} (P : DualNegativeBesovFiniteParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : ENNReal

The exact negative finite-interior hatted dual Besov seminorm.

Equations

• HCPolySupport.Book.Ch01.dualNegativeBesovFiniteHattedSeminorm P Q f hf = HCPolySupport.exactDualFiniteHattedSeminorm P Q f hf

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.dualNegativeBesovFiniteFullNorm {d : ℕ} (P : DualNegativeBesovFiniteParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : ENNReal

The exact negative finite-interior full dual Besov norm.

Equations

• HCPolySupport.Book.Ch01.dualNegativeBesovFiniteFullNorm P Q f hf = HCPolySupport.exactDualFiniteFullNorm P Q f hf

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.dualNegativeBesovTopHattedSeminorm {d : ℕ} (P : DualNegativeBesovTopParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : ENNReal

The exact negative q = ∞ hatted dual Besov seminorm.

Equations

• HCPolySupport.Book.Ch01.dualNegativeBesovTopHattedSeminorm P Q f hf = HCPolySupport.exactDualTopHattedSeminorm P Q f hf

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.dualNegativeBesovTopFullNorm {d : ℕ} (P : DualNegativeBesovTopParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : ENNReal

The exact negative q = ∞ full dual Besov norm.

Equations

• HCPolySupport.Book.Ch01.dualNegativeBesovTopFullNorm P Q f hf = HCPolySupport.exactDualTopFullNorm P Q f hf

theorem HCPolySupport.Book.Ch01.dualNegativeBesovQOneHattedSeminorm_eq {d : ℕ} (P : DualNegativeBesovQOneParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : dualNegativeBesovQOneHattedSeminorm P Q f hf = ⨆ (T : DualNegativeBesovQOneHattedTest P Q), ExactDualQOneHattedTest.pairing hf T

Formula for the exact negative q = 1 hatted dual Besov seminorm.

theorem HCPolySupport.Book.Ch01.dualNegativeBesovQOneFullNorm_eq {d : ℕ} (P : DualNegativeBesovQOneParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : dualNegativeBesovQOneFullNorm P Q f hf = ⨆ (T : DualNegativeBesovQOneFullTest P Q), ExactDualQOneFullTest.pairing hf T

Formula for the exact negative q = 1 full dual Besov norm.

theorem HCPolySupport.Book.Ch01.dualNegativeBesovFiniteHattedSeminorm_eq {d : ℕ} (P : DualNegativeBesovFiniteParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : dualNegativeBesovFiniteHattedSeminorm P Q f hf = ⨆ (T : DualNegativeBesovFiniteHattedTest P Q), ExactDualFiniteHattedTest.pairing hf T

Formula for the exact negative finite-interior hatted dual Besov seminorm.

theorem HCPolySupport.Book.Ch01.dualNegativeBesovFiniteFullNorm_eq {d : ℕ} (P : DualNegativeBesovFiniteParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : dualNegativeBesovFiniteFullNorm P Q f hf = ⨆ (T : DualNegativeBesovFiniteFullTest P Q), ExactDualFiniteFullTest.pairing hf T

Formula for the exact negative finite-interior full dual Besov norm.

theorem HCPolySupport.Book.Ch01.dualNegativeBesovTopHattedSeminorm_eq {d : ℕ} (P : DualNegativeBesovTopParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : dualNegativeBesovTopHattedSeminorm P Q f hf = ⨆ (T : DualNegativeBesovTopHattedTest P Q), ExactDualTopHattedTest.pairing hf T

Formula for the exact negative q = ∞ hatted dual Besov seminorm.

theorem HCPolySupport.Book.Ch01.dualNegativeBesovTopFullNorm_eq {d : ℕ} (P : DualNegativeBesovTopParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : dualNegativeBesovTopFullNorm P Q f hf = ⨆ (T : DualNegativeBesovTopFullTest P Q), ExactDualTopFullTest.pairing hf T

Formula for the exact negative q = ∞ full dual Besov norm.

Exact concrete circ negative Besov quantities

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.CircNegativeBesovFiniteParameters : Type

Parameters for the exact finite-q concrete circ Besov seminorm.

Equations

• HCPolySupport.Book.Ch01.CircNegativeBesovFiniteParameters = HCPolySupport.ExactCircFiniteParameters

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.CircNegativeBesovTopParameters : Type

Parameters for the exact q = ∞ concrete circ Besov seminorm.

Equations

• HCPolySupport.Book.Ch01.CircNegativeBesovTopParameters = HCPolySupport.ExactCircTopParameters

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.CircNegativeBesovIntegrable {d : ℕ} (Q : Cube d) (f : Vec d → ℝ) : Prop

Integrability witnesses for all disjoint block means in the exact circ lane.

Equations

• HCPolySupport.Book.Ch01.CircNegativeBesovIntegrable Q f = HCPolySupport.ExactCircIntegrable Q f

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.circNegativeBesovFiniteSeminorm {d : ℕ} (P : CircNegativeBesovFiniteParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : CircNegativeBesovIntegrable Q f) : ENNReal

The exact finite-q concrete circ negative Besov seminorm.

Equations

• HCPolySupport.Book.Ch01.circNegativeBesovFiniteSeminorm P Q f hf = HCPolySupport.exactCircFiniteSeminorm P Q f hf

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.circNegativeBesovTopSeminorm {d : ℕ} (P : CircNegativeBesovTopParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : CircNegativeBesovIntegrable Q f) : ENNReal

The exact q = ∞ concrete circ negative Besov seminorm.

Equations

• HCPolySupport.Book.Ch01.circNegativeBesovTopSeminorm P Q f hf = HCPolySupport.exactCircTopSeminorm P Q f hf

theorem HCPolySupport.Book.Ch01.circNegativeBesovFiniteSeminorm_eq {d : ℕ} (P : CircNegativeBesovFiniteParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : CircNegativeBesovIntegrable Q f) : circNegativeBesovFiniteSeminorm P Q f hf = (∑' (j : ℕ), exactCircDepthTerm Q P.s P.p f hf j ^ P.q) ^ P.q⁻¹

Formula for the exact finite-q concrete circ negative Besov seminorm.

theorem HCPolySupport.Book.Ch01.circNegativeBesovTopSeminorm_eq {d : ℕ} (P : CircNegativeBesovTopParameters) (Q : Cube d) (f : Vec d → ℝ) (hf : CircNegativeBesovIntegrable Q f) : circNegativeBesovTopSeminorm P Q f hf = ⨆ (j : ℕ), exactCircDepthTerm Q P.s P.p f hf j

Formula for the exact q = ∞ concrete circ negative Besov seminorm.

Legacy totalized and disjoint-cube compatibility vocabulary

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.normalizedAverage {d : ℕ} (Q : Cube d) (u : Vec d → ℝ) : ℝ

Legacy totalized cube average. This is not the proof-carrying Chapter 1 average.

Equations

• HCPolySupport.Book.Ch01.Legacy.normalizedAverage Q u = HCPolySupport.cubeAverage Q u

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.normalizedLpNorm {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : Cube d) (p : ENNReal) (u : Vec d → E) : ℝ

Legacy totalized cube L^p norm. This is not the exact Chapter 1 norm.

Equations

• HCPolySupport.Book.Ch01.Legacy.normalizedLpNorm Q p u = HCPolySupport.cubeLpNorm Q p u

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.positiveBesovPartialNorm {d : ℕ} (Q : Cube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) : ℝ

Legacy finite-depth positive Besov norm using disjoint descendants.

Equations

• HCPolySupport.Book.Ch01.Legacy.positiveBesovPartialNorm Q s p q N u = HCPolySupport.cubeBesovDisjointPartialNorm Q s p q N u

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.positiveBesovPartialNormTop {d : ℕ} (Q : Cube d) (s : ℝ) (p : ENNReal) (N : ℕ) (u : Vec d → ℝ) : ℝ

Legacy finite-depth positive q = ∞ Besov norm using disjoint descendants.

Equations

• HCPolySupport.Book.Ch01.Legacy.positiveBesovPartialNormTop Q s p N u = HCPolySupport.cubeBesovDisjointPartialNormTop Q s p N u

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.positiveBesovPartialSeminormTwo {d : ℕ} (Q : Cube d) (s : ℝ) (N : ℕ) (u : Vec d → ℝ) : ℝ

Legacy finite-depth positive q = 2 Besov seminorm using disjoint descendants.

Equations

• HCPolySupport.Book.Ch01.Legacy.positiveBesovPartialSeminormTwo Q s N u = HCPolySupport.cubeBesovDisjointPartialSeminorm Q s 2 2 N u

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.positiveBesovSeminormTwo {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) : ℝ

Legacy totalized infinite-depth positive q = 2 Besov seminorm.

Equations

• HCPolySupport.Book.Ch01.Legacy.positiveBesovSeminormTwo Q s u = sSup (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovDisjointPartialSeminorm Q s 2 2 N u)

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.positiveBesovPartialNormTwo {d : ℕ} (Q : Cube d) (s : ℝ) (N : ℕ) (u : Vec d → ℝ) : ℝ

Legacy finite-depth positive q = 2 Besov norm using disjoint descendants.

Equations

• HCPolySupport.Book.Ch01.Legacy.positiveBesovPartialNormTwo Q s N u = HCPolySupport.cubeBesovDisjointPartialNorm Q s 2 2 N u

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.positiveBesovNormTwo {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) : ℝ

Legacy totalized infinite-depth positive q = 2 Besov norm.

Equations

• HCPolySupport.Book.Ch01.Legacy.positiveBesovNormTwo Q s u = sSup (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovDisjointPartialNorm Q s 2 2 (N + 1) u)

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.positiveBesovLocalizeConstant (_d : ℕ) : ℝ

Legacy dimension-shaped localization constant for the disjoint positive lane.

Equations

• HCPolySupport.Book.Ch01.Legacy.positiveBesovLocalizeConstant _d = 2

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.negativeBesovLocalizeConstant (_d : ℕ) : ℝ

Legacy dimension-shaped localization constant for the totalized negative lane.

Equations

• HCPolySupport.Book.Ch01.Legacy.negativeBesovLocalizeConstant _d = 2

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.positiveBesovNormTop {d : ℕ} (Q : Cube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) : ℝ

Legacy totalized infinite-depth positive q = ∞ Besov norm.

Equations

• HCPolySupport.Book.Ch01.Legacy.positiveBesovNormTop Q s p u = sSup (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovDisjointPartialNormTop Q s p (N + 1) u)

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.positiveBesovVectorNormTop {d : ℕ} (Q : Cube d) (s : ℝ) (p : ENNReal) (u : Vec d → Vec d) : ℝ

Legacy componentwise vector-valued positive q = ∞ Besov norm. The manuscript does not select this componentwise convention.

Equations

• HCPolySupport.Book.Ch01.Legacy.positiveBesovVectorNormTop Q s p u = ∑ i : Fin d, HCPolySupport.Book.Ch01.Legacy.positiveBesovNormTop Q s p fun (x : HCPolySupport.Book.Ch01.Vec d) => u x i

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.circNegativeBesovNorm {d : ℕ} (Q : Cube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) : ℝ

Legacy totalized concrete circ negative Besov norm.

Equations

• HCPolySupport.Book.Ch01.Legacy.circNegativeBesovNorm Q s p q u = HCPolySupport.cubeBesovCircNorm Q s p q u

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.circNegativeBesovPartialNorm {d : ℕ} (Q : Cube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) : ℝ

Legacy finite-depth totalized concrete circ negative Besov norm.

Equations

• HCPolySupport.Book.Ch01.Legacy.circNegativeBesovPartialNorm Q s p q N u = HCPolySupport.cubeBesovCircPartialNorm Q s p q N u

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.dualNegativeBesovSeminorm {d : ℕ} (Q : Cube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) : ℝ

Legacy totalized mean-zero dual negative Besov seminorm.

Equations

• HCPolySupport.Book.Ch01.Legacy.dualNegativeBesovSeminorm Q s p q u = HCPolySupport.cubeBesovDualMeanZeroSeminorm Q s p q u

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.dualNegativeBesovNorm {d : ℕ} (Q : Cube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) : ℝ

Legacy totalized full dual negative Besov norm.

Equations

• HCPolySupport.Book.Ch01.Legacy.dualNegativeBesovNorm Q s p q u = HCPolySupport.cubeBesovDualFullNorm Q s p q u