Main definitions

• ScaledReal ν n: ℝ with norm |x| · νⁿ

Positive Reals

@[reducible, inline]

abbrev PosReal : Type

Positive real numbers asx a subtype

Equations

• PosReal = { x : ℝ // 0 < x }

instance PosReal.instCoeReal : Coe PosReal ℝ

Equations

• PosReal.instCoeReal = { coe := Subtype.val }

@[simp]

theorem PosReal.coe_pos (ν : PosReal) : 0 < ↑ν

@[simp]

theorem PosReal.coe_nonneg (ν : PosReal) : 0 ≤ ↑ν

@[simp]

theorem PosReal.coe_ne_zero (ν : PosReal) : ↑ν ≠ 0

def PosReal.toNNReal (ν : PosReal) : NNReal

Equations

• ν.toNNReal = ⟨↑ν, ⋯⟩

Scaled Real Numbers

ScaledReal ν n is ℝ with norm ‖x‖ = |x| · νⁿ.

The parameters ν and n are not used in the definition (which is just ℝ), but they create distinct types with different Norm instances via inferInstanceAs. This allows lp (ScaledReal ν) 1 to compute the weighted norm Σₙ |aₙ| νⁿ automatically.

def ScaledReal (_ν : PosReal) (_n : ℕ) : Type

ℝ with scaled norm at index n: ‖x‖ = |x| · νⁿ

Equations

• ScaledReal _ν _n = ℝ

instance ScaledReal.instAddCommGroup {ν : PosReal} {n : ℕ} : AddCommGroup (ScaledReal ν n)

Borrow algebraic instances from ℝ

Equations

• ScaledReal.instAddCommGroup = inferInstanceAs (AddCommGroup ℝ)

instance ScaledReal.instModuleReal {ν : PosReal} {n : ℕ} : Module ℝ (ScaledReal ν n)

Equations

• ScaledReal.instModuleReal = inferInstanceAs (Module ℝ ℝ)

instance ScaledReal.instRing {ν : PosReal} {n : ℕ} : Ring (ScaledReal ν n)

Equations

• ScaledReal.instRing = inferInstanceAs (Ring ℝ)

instance ScaledReal.instLattice {ν : PosReal} {n : ℕ} : Lattice (ScaledReal ν n)

Equations

• ScaledReal.instLattice = inferInstanceAs (Lattice ℝ)

instance ScaledReal.instLinearOrder {ν : PosReal} {n : ℕ} : LinearOrder (ScaledReal ν n)

Equations

• ScaledReal.instLinearOrder = inferInstanceAs (LinearOrder ℝ)

instance ScaledReal.instAddLeftMono {ν : PosReal} {n : ℕ} : AddLeftMono (ScaledReal ν n)

def ScaledReal.toReal {ν : PosReal} {n : ℕ} (x : ScaledReal ν n) : ℝ

Cast to ℝ (identity map)

Equations

• ↑x = x

instance ScaledReal.instCoeOutReal {ν : PosReal} {n : ℕ} : CoeOut (ScaledReal ν n) ℝ

Coercion from ScaledReal to ℝ. This is the identity since ScaledReal is definitionally ℝ.

Equations

• ScaledReal.instCoeOutReal = { coe := ScaledReal.toReal }

instance ScaledReal.instNorm {ν : PosReal} {n : ℕ} : Norm (ScaledReal ν n)

The instance of type Norm for ScaledReal: ‖x‖ = |x| · νⁿ

Equations

• ScaledReal.instNorm = { norm := fun (x : ScaledReal ν n) => |↑x| * ↑ν ^ n }

theorem ScaledReal.norm_def {ν : PosReal} {n : ℕ} (x : ScaledReal ν n) : ‖x‖ = |↑x| * ↑ν ^ n

theorem ScaledReal.norm_nonneg' {ν : PosReal} {n : ℕ} (x : ScaledReal ν n) : 0 ≤ ‖x‖

@[simp]

theorem ScaledReal.norm_zero' {ν : PosReal} {n : ℕ} : ‖0‖ = 0

@[simp]

theorem ScaledReal.norm_neg' {ν : PosReal} {n : ℕ} (x : ScaledReal ν n) : ‖-x‖ = ‖x‖

theorem ScaledReal.norm_add_le' {ν : PosReal} {n : ℕ} (x y : ScaledReal ν n) : ‖x + y‖ ≤ ‖x‖ + ‖y‖

theorem ScaledReal.norm_smul' {ν : PosReal} {n : ℕ} (c : ℝ) (x : ScaledReal ν n) : ‖c • x‖ = |c| * ‖x‖

theorem ScaledReal.norm_eq_zero' {ν : PosReal} {n : ℕ} (x : ScaledReal ν n) : ‖x‖ = 0 ↔ x = 0

instance ScaledReal.instNormedAddCommGroup {ν : PosReal} {n : ℕ} : NormedAddCommGroup (ScaledReal ν n)

ScaledReal ν n is a normed abelian group.

This instance establishes that ScaledReal ν n is a metric space where the distance is induced by the norm: d(x, y) = ‖x - y‖.

Required properties:

• dist_self: d(x, x) = 0
• dist_comm: d(x, y) = d(y, x)
• dist_triangle: d(x, z) ≤ d(x, y) + d(y, z)
• eq_of_dist_eq_zero: d(x, y) = 0 → x = y

This is a prerequisite for NormedSpace and enables the use of ScaledReal in Mathlib's lp space construction.

Equations

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

instance ScaledReal.instNormedSpace {ν : PosReal} {n : ℕ} : NormedSpace ℝ (ScaledReal ν n)

ScaledReal ν n is a normed vector space over ℝ.

This instance proves that scalar multiplication is compatible with the norm: ‖c • x‖ = |c| · ‖x‖

Together with instNormedAddCommGroup, this makes ScaledReal ν n a normed space, enabling:

• Use as fiber type in lp (ScaledReal ν) p for weighted ℓᵖ spaces
• Completeness (Banach space structure inherited from ℝ)
• Continuous linear maps and Fréchet derivatives
• Integration with Mathlib's analysis library

Equations

• ScaledReal.instNormedSpace = { toModule := ScaledReal.instModuleReal, norm_smul_le := ⋯ }

instance ScaledReal.instFiniteDimensional {ν : PosReal} {n : ℕ} : FiniteDimensional ℝ (ScaledReal ν n)

ScaledReal ν n is finite-dimensional over ℝ since it is just ℝ with a rescaled norm.

instance ScaledReal.instCompleteSpace {ν : PosReal} {n : ℕ} : CompleteSpace (ScaledReal ν n)

Completeness of ScaledReal ν n, inherited from finite dimensionality.

def ScaledReal.ofReal {ν : PosReal} {n : ℕ} : ℝ ≃+ ScaledReal ν n

Additive isomorphism from ℝ to ScaledReal

Equations

• ScaledReal.ofReal = AddEquiv.refl ℝ

@[simp]

theorem ScaledReal.toReal_apply {ν : PosReal} {n : ℕ} (x : ScaledReal ν n) : ↑x = x

@[simp]

theorem ScaledReal.ofReal_apply {ν : PosReal} {n : ℕ} (x : ℝ) : ofReal x = x

@[simp]

theorem ScaledReal.coe_zero {ν : PosReal} {n : ℕ} : 0 = 0

@[simp]

theorem ScaledReal.coe_one {ν : PosReal} {n : ℕ} : 1 = 1

@[simp]

theorem ScaledReal.coe_add {ν : PosReal} {n : ℕ} (x y : ScaledReal ν n) : x + y = x + y

@[simp]

theorem ScaledReal.coe_sub {ν : PosReal} {n : ℕ} (x y : ScaledReal ν n) : x - y = x - y

@[simp]

theorem ScaledReal.coe_neg {ν : PosReal} {n : ℕ} (x : ScaledReal ν n) : -x = -x

@[simp]

theorem ScaledReal.coe_mul {ν : PosReal} {n : ℕ} (x y : ScaledReal ν n) : x * y = x * y