Uniqueness for resolvents on bounded measurable functions

This file proves three elementary contraction principles for maps acting on bounded measurable real functions. The first gives uniqueness for a bounded multiplicative perturbation equation. The second propagates equality of two resolvent families from all sufficiently large shifts to every positive shift by the resolvent identity. The third combines the first two principles.

Main results: perturbed_unique, resolventFamily_eq_of_eventually, and perturbed_eq_of_resolventFamilies.

The operators are plain maps on functions; no Banach-space carrier or continuity is asserted.

theorem MarkovProcess.perturbed_unique {alpha : Type u_1} [MeasurableSpace alpha] [Nonempty alpha] (R X Y : (alpha → ℝ) → alpha → ℝ) {q : alpha → ℝ} {C lam : ℝ} (hR_add : ∀ {f g : alpha → ℝ}, Measurable f → Measurable g → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → (∃ (D : ℝ), ∀ (x : alpha), |g x| ≤ D) → R (f + g) = R f + R g) (hR_bound : ∀ {f : alpha → ℝ}, Measurable f → ∀ {D : ℝ}, (∀ (x : alpha), |f x| ≤ D) → ∀ (x : alpha), |R f x| ≤ D / lam) (hq : Measurable q) (hq0 : ∀ (x : alpha), 0 ≤ q x) (hqC : ∀ (x : alpha), q x ≤ C) (hlam : C < lam) (hX_meas : ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → Measurable (X f)) (hY_meas : ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → Measurable (Y f)) (hX_bound : ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → ∃ (D : ℝ), ∀ (x : alpha), |X f x| ≤ D) (hY_bound : ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → ∃ (D : ℝ), ∀ (x : alpha), |Y f x| ≤ D) (hX_fixed : ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → X f = R f - R fun (x : alpha) => q x * X f x) (hY_fixed : ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → Y f = R f - R fun (x : alpha) => q x * Y f x) {f : alpha → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : alpha), |f x| ≤ D) : X f = Y f

Uniqueness for a bounded perturbation equation. Suppose R is additive on bounded measurable functions and has the uniform bound |R f x| ≤ D / λ whenever |f| ≤ D. If 0 ≤ q ≤ C and C < λ, then two maps preserving bounded measurable functions and solving Z f = R f - R (q * Z f) agree on every bounded measurable function.

At a fixed sufficiently large shift, this gives the bounded-measurable equality needed by resolventFamily_eq_of_eventually. The Nonempty alpha assumption is used to extract 0 ≤ C and nonnegativity of bounds from their pointwise hypotheses.

theorem MarkovProcess.resolventFamily_eq_of_eventually {alpha : Type u_1} [MeasurableSpace alpha] [Nonempty alpha] (X Y : ℝ → (alpha → ℝ) → alpha → ℝ) (C : ℝ) (hX_add : ∀ {lam : ℝ}, 0 < lam → ∀ {f g : alpha → ℝ}, Measurable f → Measurable g → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → (∃ (D : ℝ), ∀ (x : alpha), |g x| ≤ D) → X lam (f + g) = X lam f + X lam g) (hX_meas : ∀ {lam : ℝ}, 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → Measurable (X lam f)) (hY_meas : ∀ {lam : ℝ}, 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → Measurable (Y lam f)) (hX_bound : ∀ {lam : ℝ}, 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → ∀ {D : ℝ}, (∀ (x : alpha), |f x| ≤ D) → ∀ (x : alpha), |X lam f x| ≤ D / lam) (hY_bound : ∀ {lam : ℝ}, 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → ∃ (D : ℝ), ∀ (x : alpha), |Y lam f x| ≤ D) (hX_resolvent : ∀ {mu lam : ℝ}, 0 < mu → 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → X mu f = X lam f + (lam - mu) • X lam (X mu f)) (hY_resolvent : ∀ {mu lam : ℝ}, 0 < mu → 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → Y mu f = Y lam f + (lam - mu) • Y lam (Y mu f)) (hlarge : ∀ {lam : ℝ}, C < lam → 0 < lam → ∀ {g : alpha → ℝ}, Measurable g → (∃ (D : ℝ), ∀ (x : alpha), |g x| ≤ D) → X lam g = Y lam g) {mu : ℝ} (hmu : 0 < mu) {f : alpha → ℝ} (hfMeas : Measurable f) {D : ℝ} (hfD : ∀ (x : alpha), |f x| ≤ D) : X mu f = Y mu f

Equality of resolvent families from equality at large shifts. Let X and Y be families of maps on bounded measurable real functions. Suppose X is additive and satisfies the bound |X_λ f| ≤ D / λ, while both families preserve measurability and boundedness. If both satisfy the resolvent identity and agree on bounded measurable functions above a fixed threshold, then they agree on bounded measurable functions at every positive shift.

The large-shift equality need only hold at the bounded measurable arguments used by the proof.

theorem MarkovProcess.perturbed_eq_of_resolventFamilies {alpha : Type u_1} [MeasurableSpace alpha] [Nonempty alpha] (R X Y : ℝ → (alpha → ℝ) → alpha → ℝ) {q : alpha → ℝ} {C : ℝ} (hR_add : ∀ {lam : ℝ}, C < lam → 0 < lam → ∀ {f g : alpha → ℝ}, Measurable f → Measurable g → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → (∃ (D : ℝ), ∀ (x : alpha), |g x| ≤ D) → R lam (f + g) = R lam f + R lam g) (hR_bound : ∀ {lam : ℝ}, C < lam → 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → ∀ {D : ℝ}, (∀ (x : alpha), |f x| ≤ D) → ∀ (x : alpha), |R lam f x| ≤ D / lam) (hq : Measurable q) (hq0 : ∀ (x : alpha), 0 ≤ q x) (hqC : ∀ (x : alpha), q x ≤ C) (hX_add : ∀ {lam : ℝ}, 0 < lam → ∀ {f g : alpha → ℝ}, Measurable f → Measurable g → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → (∃ (D : ℝ), ∀ (x : alpha), |g x| ≤ D) → X lam (f + g) = X lam f + X lam g) (hX_meas : ∀ {lam : ℝ}, 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → Measurable (X lam f)) (hY_meas : ∀ {lam : ℝ}, 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → Measurable (Y lam f)) (hX_bound : ∀ {lam : ℝ}, 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → ∀ {D : ℝ}, (∀ (x : alpha), |f x| ≤ D) → ∀ (x : alpha), |X lam f x| ≤ D / lam) (hY_bound : ∀ {lam : ℝ}, 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → ∃ (D : ℝ), ∀ (x : alpha), |Y lam f x| ≤ D) (hX_resolvent : ∀ {mu lam : ℝ}, 0 < mu → 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → X mu f = X lam f + (lam - mu) • X lam (X mu f)) (hY_resolvent : ∀ {mu lam : ℝ}, 0 < mu → 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → Y mu f = Y lam f + (lam - mu) • Y lam (Y mu f)) (hX_fixed : ∀ {lam : ℝ}, C < lam → 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → X lam f = R lam f - R lam fun (x : alpha) => q x * X lam f x) (hY_fixed : ∀ {lam : ℝ}, C < lam → 0 < lam → ∀ {f : alpha → ℝ}, Measurable f → (∃ (D : ℝ), ∀ (x : alpha), |f x| ≤ D) → Y lam f = R lam f - R lam fun (x : alpha) => q x * Y lam f x) {lam : ℝ} (hlam : 0 < lam) {f : alpha → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : alpha), |f x| ≤ D) : X lam f = Y lam f

Equality of perturbed resolvent families. Two resolvent families that satisfy the same bounded perturbation equation above the potential bound agree on every bounded measurable function at every positive shift. The first family must be additive and contractive; the second need only preserve boundedness. Both preserve measurability and satisfy the resolvent identity.