Change of variables (docs/roleflow.tex, sec:cov)

Cov μ ν f J says that f pushes J · μ forward to ν. The development needs four rules: Cov.pres (measure-preserving maps), Cov.comp, Cov.tri (triangular maps, by Tonelli) and Cov.inv (the inverse, with the negated log-weight). Weights are usually expw ℓ = e^ℓ for a real log-weight ℓ. Also generic: Cov.congr_ae (the weight matters only almost everywhere), Cov.pres_comp and Cov.comp_pres (composing with a measure-preserving map) and MeasurePreserving.of_inverse.

The second half is about products indexed by finite types with one measure per sort: the measure-preserving reorders measurePreserving_reorder, which rename coordinates along a bijection of index types and transport each coordinate along an equality of sorts. Contexts (Val in RoleFlow.Sig) and the live states of the density proof are such products.

noncomputable def RoleFlow.expw (t : ℝ) : ENNReal

The weight e^t as an extended nonnegative real.

Equations

• RoleFlow.expw t = ENNReal.ofReal (Real.exp t)

theorem RoleFlow.measurable_expw : Measurable expw

@[simp]

theorem RoleFlow.expw_zero : expw 0 = 1

theorem RoleFlow.expw_add (a b : ℝ) : expw (a + b) = expw a * expw b

theorem RoleFlow.expw_neg_mul (a : ℝ) : expw (-a) * expw a = 1

def RoleFlow.Cov {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (f : X → Y) (J : X → ENNReal) : Prop

f pushes J · μ forward to ν: integrating φ ∘ f against J is integrating φ.

Equations

• RoleFlow.Cov μ ν f J = ∀ (φ : Y → ENNReal), Measurable φ → ∫⁻ (x : X), φ (f x) * J x ∂μ = ∫⁻ (y : Y), φ y ∂ν

theorem RoleFlow.Cov.congr {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {f f' : X → Y} {J J' : X → ENNReal} (hf : ∀ (x : X), f x = f' x) (hJ : ∀ (x : X), J x = J' x) (h : Cov μ ν f J) : Cov μ ν f' J'

theorem RoleFlow.Cov.congr_ae {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {f : X → Y} {J J' : X → ENNReal} (hJ : J =ᵐ[μ] J') (h : Cov μ ν f J) : Cov μ ν f J'

The weight matters only almost everywhere.

theorem RoleFlow.Cov.pres {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {f : X → Y} (hf : MeasureTheory.MeasurePreserving f μ ν) : Cov μ ν f fun (x : X) => 1

Pres: a measure-preserving map has weight 1.

theorem RoleFlow.Cov.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {τ : MeasureTheory.Measure Z} {f : X → Y} {g : Y → Z} {J : X → ENNReal} {K : Y → ENNReal} (hg : Measurable g) (hK : Measurable K) (h₁ : Cov μ ν f J) (h₂ : Cov ν τ g K) : Cov μ τ (fun (x : X) => g (f x)) fun (x : X) => J x * K (f x)

Comp: weights multiply along composition.

theorem RoleFlow.Cov.tri {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {τ : MeasureTheory.Measure Z} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite τ] {g : X → Y → Z} {J : X → Y → ENNReal} (hg : Measurable fun (q : X × Y) => g q.1 q.2) (hJ : Measurable fun (q : X × Y) => J q.1 q.2) (h : ∀ (p : X), Cov ν τ (g p) (J p)) : Cov (μ.prod ν) (μ.prod τ) (fun (q : X × Y) => (q.1, g q.1 q.2)) fun (q : X × Y) => J q.1 q.2

Tri: the triangular map (p, a) ↦ (p, g p a), by Tonelli and the fibre at each p. Only joint measurability is needed, no derivative in the parameter.

theorem RoleFlow.Cov.inv {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {f : X → Y} {g : Y → X} {ℓ : X → ℝ} (hg : Measurable g) (hℓ : Measurable ℓ) (hgf : ∀ (x : X), g (f x) = x) (h : Cov μ ν f fun (x : X) => expw (ℓ x)) : Cov ν μ g fun (y : Y) => expw (-ℓ (g y))

Inv: a left inverse g of f pushes ν back with the negated log-weight. Only the left law g ∘ f = id is needed: ν lives on the range of f, where g is determined. Since the log-weight is real, no reciprocity or nonvanishing hypothesis appears.

theorem RoleFlow.Cov.pres_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {τ : MeasureTheory.Measure Z} {f : X → Y} {g : Y → Z} {K : Y → ENNReal} (hf : MeasureTheory.MeasurePreserving f μ ν) (hg : Measurable g) (hK : Measurable K) (h : Cov ν τ g K) : Cov μ τ (fun (x : X) => g (f x)) fun (x : X) => K (f x)

theorem RoleFlow.Cov.comp_pres {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {τ : MeasureTheory.Measure Z} {f : X → Y} {J : X → ENNReal} {g : Y → Z} (h : Cov μ ν f J) (hg : MeasureTheory.MeasurePreserving g ν τ) : Cov μ τ (fun (x : X) => g (f x)) J

theorem RoleFlow.Cov.map_eq {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {f : X → Y} {g : Y → X} {J : X → ENNReal} (hg : Measurable g) (hgf : ∀ (x : X), g (f x) = x) (h : Cov μ ν f J) : MeasureTheory.Measure.map g ν = μ.withDensity J

With a measurable left inverse g, J is the density of g_* ν with respect to μ.

theorem MeasureTheory.MeasurePreserving.of_inverse {Y : Type u_1} {Z : Type u_2} [MeasurableSpace Y] [MeasurableSpace Z] {μ' : Measure Y} {ν' : Measure Z} {f : Z → Y} {g : Y → Z} (hg : MeasurePreserving g μ' ν') (hf : Measurable f) (hfg : ∀ (y : Y), f (g y) = y) : MeasurePreserving f ν' μ'

If g preserves measure and f is a measurable two-sided inverse, f preserves measure.

Products with one measure per sort, and reorders

def RoleFlow.tr {S : Type u_1} (X : S → Type u_2) {a b : S} (h : a = b) (x : X a) : X b

Transport along an equality of sorts.

Equations

• RoleFlow.tr X h x = h ▸ x

@[simp]

theorem RoleFlow.tr_rfl {S : Type u_1} {X : S → Type u_2} {a : S} (x : X a) : tr X ⋯ x = x

@[simp]

theorem RoleFlow.tr_tr {S : Type u_1} {X : S → Type u_2} {a b c : S} (h : a = b) (h' : b = c) (x : X a) : tr X h' (tr X h x) = tr X ⋯ x

theorem RoleFlow.tr_apply_eq {S : Type u_1} {X : S → Type u_2} {ι : Type u_3} {σ : ι → S} (s : (i : ι) → X (σ i)) {i j : ι} (hij : i = j) (h : σ i = σ j) : tr X h (s i) = s j

Transport along an equality of values of a family.

theorem RoleFlow.measurable_tr {S : Type u_1} {X : S → Type u_2} [(s : S) → MeasurableSpace (X s)] {a b : S} (h : a = b) : Measurable (tr X h)

theorem RoleFlow.measurePreserving_tr {S : Type u_1} {X : S → Type u_2} [(s : S) → MeasurableSpace (X s)] (μ : (s : S) → MeasureTheory.Measure (X s)) {a b : S} (h : a = b) : MeasureTheory.MeasurePreserving (tr X h) (μ a) (μ b)

def RoleFlow.reorderEquiv {S : Type u_1} {X : S → Type u_2} [(s : S) → MeasurableSpace (X s)] {ι : Type u_3} {κ : Type u_4} (α : ι → S) (β : κ → S) (e : ι ≃ κ) (h : ∀ (i : ι), β (e i) = α i) : ((k : κ) → X (β k)) ≃ᵐ ((i : ι) → X (α i))

Reorder: rename the coordinates of a product along a bijection e, transporting each along the equality of its sorts.

Equations

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

theorem RoleFlow.measurePreserving_reorder {S : Type u_1} {X : S → Type u_2} [(s : S) → MeasurableSpace (X s)] (μ : (s : S) → MeasureTheory.Measure (X s)) [∀ (s : S), MeasureTheory.SigmaFinite (μ s)] {ι : Type u_3} {κ : Type u_4} [Fintype ι] [Fintype κ] (α : ι → S) (β : κ → S) (e : ι ≃ κ) (h : ∀ (i : ι), β (e i) = α i) : MeasureTheory.MeasurePreserving (⇑(reorderEquiv α β e h)) (MeasureTheory.Measure.pi fun (k : κ) => μ (β k)) (MeasureTheory.Measure.pi fun (i : ι) => μ (α i))

Reorder preserves the product measure.