Coarse-graining support: Support.Sobolev.FiniteLpExponent

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

Finite L^p exponents and Euclidean cube fields

This module provides the exact finite-exponent carrier used by the Chapter 3 analytic kernels, together with restriction of a Euclidean L^p field to a subcube while retaining its same pointwise representative.

structure HCPolySupport.FiniteLpExponent : Type

An extended nonnegative real exponent strictly between one and infinity.

• exponent : ENNReal

  The finite exponent greater than one.

• one_lt : 1 < self.exponent
• lt_top : self.exponent < ⊤

noncomputable def HCPolySupport.FiniteLpExponent.conjugate (p : FiniteLpExponent) : FiniteLpExponent

The Hölder conjugate exponent, again strictly between one and infinity.

Equations

• p.conjugate = { exponent := p.exponent.conjExponent, one_lt := ⋯, lt_top := ⋯ }

theorem HCPolySupport.FiniteLpExponent.holderConjugate (p : FiniteLpExponent) : p.exponent.HolderConjugate p.conjugate.exponent

@[simp]

theorem HCPolySupport.FiniteLpExponent.conjugate_conjugate (p : FiniteLpExponent) : p.conjugate.conjugate = p

noncomputable def HCPolySupport.FiniteLpExponent.two : FiniteLpExponent

The finite exponent two.

Equations

• HCPolySupport.FiniteLpExponent.two = { exponent := 2, one_lt := HCPolySupport.FiniteLpExponent.two._proof_1, lt_top := HCPolySupport.FiniteLpExponent.two._proof_2 }

@[simp]

theorem HCPolySupport.FiniteLpExponent.two_exponent : two.exponent = 2

@[simp]

theorem HCPolySupport.FiniteLpExponent.conjugate_two : two.conjugate = two

noncomputable def HCPolySupport.fractionalOrderHalf (s : ↑FractionalOrder) : ↑FractionalOrder

Halving preserves the open interval of fractional orders.

Equations

• HCPolySupport.fractionalOrderHalf s = ⟨↑s / 2, ⋯⟩

@[simp]

theorem HCPolySupport.fractionalOrderHalf_value (s : ↑FractionalOrder) : ↑(fractionalOrderHalf s) = ↑s / 2

structure HCPolySupport.CubeEuclideanLpField {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) : Type

A vector field with finite Euclidean Lᵖ seminorm for normalized cube measure.

• toField : Vec d → Vec d

  The pointwise vector-valued representative of the integrable field.

• euclideanMemLp : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (self.toField x)) p.exponent (normalizedCubeMeasure Q)

@[instance_reducible]

instance HCPolySupport.CubeEuclideanLpField.instCoeFunForallVec {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} : CoeFun (CubeEuclideanLpField Q p) fun (x : CubeEuclideanLpField Q p) => Vec d → Vec d

Equations

• HCPolySupport.CubeEuclideanLpField.instCoeFunForallVec = { coe := fun (F : HCPolySupport.CubeEuclideanLpField Q p) => F.toField }

noncomputable def HCPolySupport.CubeEuclideanLpField.restrictToSubcube {d : ℕ} {Q R : TriadicCube d} {p : FiniteLpExponent} (F : CubeEuclideanLpField Q p) (hRQ : openCubeSet R ⊆ openCubeSet Q) : CubeEuclideanLpField R p

Regard the same pointwise field as an Lᵖ field on a contained open cube.

Equations

• F.restrictToSubcube hRQ = { toField := F.toField, euclideanMemLp := ⋯ }

@[simp]

theorem HCPolySupport.CubeEuclideanLpField.restrictToSubcube_toField {d : ℕ} {Q R : TriadicCube d} {p : FiniteLpExponent} (F : CubeEuclideanLpField Q p) (hRQ : openCubeSet R ⊆ openCubeSet Q) : (F.restrictToSubcube hRQ).toField = F.toField