Multiplicative Haar Measure on ℝ₊*

Defines the multiplicative Haar measure d*x = dx/x on ℝ₊* = (0, ∞) as the pushforward of Lebesgue measure under exp : ℝ → ℝ₊*. Establishes the exponential-logarithm equivalence and measure preservation under division.

Reference: lamportform.tex, Section 1, lines 94–101.

The type of positive reals

@[reducible, inline]

abbrev ConnesLean.RPos : Type

The type of positive reals R_+* = (0, ∞), the multiplicative group underlying the Haar measure d*x = dx/x. We use a subtype of ℝ for compatibility with Mathlib's measure theory and analysis libraries.

Equations

• ConnesLean.RPos = { x : ℝ // 0 < x }

instance ConnesLean.RPos.instOne : One RPos

Equations

• ConnesLean.RPos.instOne = { one := ⟨1, ConnesLean.RPos.instOne._proof_1⟩ }

instance ConnesLean.RPos.instMul : Mul RPos

Equations

• ConnesLean.RPos.instMul = { mul := fun (a b : ConnesLean.RPos) => ⟨↑a * ↑b, ⋯⟩ }

instance ConnesLean.RPos.instInv : Inv RPos

Equations

• ConnesLean.RPos.instInv = { inv := fun (a : ConnesLean.RPos) => ⟨(↑a)⁻¹, ⋯⟩ }

instance ConnesLean.RPos.instDiv : Div RPos

Equations

• ConnesLean.RPos.instDiv = { div := fun (a b : ConnesLean.RPos) => ⟨↑a / ↑b, ⋯⟩ }

def ConnesLean.RPos.toReal (x : RPos) : ℝ

The inclusion of RPos into ℝ.

Equations

• x.toReal = ↑x

@[simp]

theorem ConnesLean.RPos.toReal_pos (x : RPos) : 0 < ↑x

@[simp]

theorem ConnesLean.RPos.toReal_ne_zero (x : RPos) : ↑x ≠ 0

@[simp]

theorem ConnesLean.RPos.one_val : ↑1 = 1

@[simp]

theorem ConnesLean.RPos.mul_val (a b : RPos) : ↑(a * b) = ↑a * ↑b

@[simp]

theorem ConnesLean.RPos.inv_val (a : RPos) : ↑a⁻¹ = (↑a)⁻¹

@[simp]

theorem ConnesLean.RPos.div_val (a b : RPos) : ↑(a / b) = ↑a / ↑b

instance ConnesLean.RPos.instTopologicalSpace : TopologicalSpace RPos

Equations

• ConnesLean.RPos.instTopologicalSpace = instTopologicalSpaceSubtype

instance ConnesLean.RPos.instMeasurableSpace : MeasurableSpace RPos

Equations

• ConnesLean.RPos.instMeasurableSpace = Subtype.instMeasurableSpace

Exponential and logarithmic maps

def ConnesLean.expToRPos (u : ℝ) : RPos

The exponential map from ℝ to RPos, serving as the logarithmic coordinate change. This is the key isomorphism: (ℝ, +, dx) ≅ (R_+*, ×, d*x).

Equations

• ConnesLean.expToRPos u = ⟨Real.exp u, ⋯⟩

def ConnesLean.logFromRPos (x : RPos) : ℝ

The logarithmic map from RPos to ℝ, inverse of expToRPos.

Equations

• ConnesLean.logFromRPos x = Real.log ↑x

@[simp]

theorem ConnesLean.logFromRPos_expToRPos (u : ℝ) : logFromRPos (expToRPos u) = u

@[simp]

theorem ConnesLean.expToRPos_logFromRPos (x : RPos) : expToRPos (logFromRPos x) = x

theorem ConnesLean.expToRPos_sub_log (u : ℝ) (a : RPos) : expToRPos u / a = expToRPos (u - logFromRPos a)

Division by a on RPos conjugates to subtraction of log a on ℝ via exp.

theorem ConnesLean.measurable_expToRPos : Measurable expToRPos

Measurability of the exponential map to RPos.

theorem ConnesLean.measurable_logFromRPos : Measurable logFromRPos

Measurability of the logarithmic map from RPos.

def ConnesLean.expEquivRPos : ℝ ≃ᵐ RPos

The measurable equivalence between ℝ and RPos via exp/log.

Equations

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

The multiplicative Haar measure

def ConnesLean.haarMult : MeasureTheory.Measure RPos

The multiplicative Haar measure on R_+*, defined as the pushforward of Lebesgue measure under exp. This gives d*x = dx/x because: ∫ f(x) d(map exp vol)(x) = ∫ f(exp u) du, and du = dx/x.

Equations

• ConnesLean.haarMult = MeasureTheory.Measure.map ConnesLean.expToRPos MeasureTheory.volume

instance ConnesLean.haarMult_sigmaFinite : MeasureTheory.SigmaFinite haarMult

The multiplicative Haar measure is sigma-finite, inherited from the sigma-finiteness of Lebesgue measure on ℝ.

theorem ConnesLean.haarMult_mul_invariant (a : RPos) (S : Set RPos) (hS : MeasurableSet S) : haarMult ((fun (x : RPos) => a * x) '' S) = haarMult S

Left-invariance of the Haar measure under multiplication: for any a ∈ R_+* and measurable S ⊆ R_+*, μ(a · S) = μ(S).

Reference: lamportform.tex, Section 1, line 99: d*(x/a) = d*x.

Division equivalence and measure preservation

def ConnesLean.rpDivEquiv (a : RPos) : RPos ≃ᵐ RPos

The measurable equivalence x ↦ x / a on RPos, with inverse x ↦ x * a. This is the core change-of-variables map underlying dilation operators and convolution identities on (R_+*, d*x).

Equations

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

@[simp]

theorem ConnesLean.rpDivEquiv_apply (a y : RPos) : (rpDivEquiv a) y = y / a

theorem ConnesLean.measurePreserving_rpDiv (a : RPos) : MeasureTheory.MeasurePreserving (⇑(rpDivEquiv a)) haarMult haarMult

Division by a preserves the multiplicative Haar measure on RPos. This is the change-of-variables identity d*(x/a) = d*x, proved by conjugating through exp to Lebesgue translation invariance on ℝ.