PrefixFactorization.lean

1import Mathlib.Topology.MetricSpace.Lipschitz2import Mathlib.Analysis.Real.Sqrt34/-! # Nonexpansive rules descend to the prefixes which actually occur -/56namespace BFPP78set_option autoImplicit false910theorem exists_nonexpansive_factor {X Y : Type*} [PseudoMetricSpace Y]11    (f : X → ℝ) (G : X → Y) (h : ∀ x y, dist (f x) (f y) ≤ dist (G x) (G y)) :12    ∃ Φ : Set.range G → ℝ, LipschitzWith 1 Φ ∧13      ∀ x, Φ ⟨G x, Set.mem_range_self x⟩ = f x := by14  classical15  let Φ : Set.range G → ℝ := fun y => f y.property.choose16  refine ⟨Φ, ?_, ?_⟩17  · apply LipschitzWith.of_dist_le_mul18    intro y z19    simp only [NNReal.coe_one, one_mul]20    have hh := h y.property.choose z.property.choose21    rw [y.property.choose_spec, z.property.choose_spec] at hh22    exact hh23  · intro x24    change f (Set.mem_range_self (f := G) x).choose = f x25    apply dist_le_zero.mp26    have hh := h (Set.mem_range_self (f := G) x).choose x27    rw [(Set.mem_range_self (f := G) x).choose_spec, dist_self] at hh28    exact hh2930end BFPP

SHA-256