IteratedClosureOnRange

formal source

  71/-- The structural closure property derived from the four Aristotelian
  72laws plus the route-independence equation: the combining rule on
  73`Range(F)` is closed under iteration in this technical sense. -/
  74def IteratedClosureOnRange (F : ℝ → ℝ) (Phi : ℝ → ℝ → ℝ) : Prop :=
  75  ClosedUnderIteration Phi (Set.image F (Set.Ioi 0))
  76
  77/-! ## Provable Consequences
  78
  79The next two lemmas extract regularity properties from closure-under-iteration
  80that are used in the conjecture's proof.  Both are fully proved here.
  81-/
  82
  83/-- **The diagonal of Φ on Range(F) is continuous.**  Pure consequence of
  84joint continuity of Φ on Range(F)². -/
  85theorem diagonal_continuous_on_range
  86    (F : ℝ → ℝ) (Phi : ℝ → ℝ → ℝ)
  87    (hClosed : IteratedClosureOnRange F Phi) :
  88    ContinuousOn (fun v : ℝ => Phi v v) (Set.image F (Set.Ioi 0)) := by
  89  obtain ⟨hCont, _⟩ := hClosed
  90  -- The diagonal map v ↦ (v, v) is continuous everywhere; compose with Phi.
  91  have h_diag_on : ContinuousOn (fun w : ℝ => ((w, w) : ℝ × ℝ))
  92      (Set.image F (Set.Ioi 0)) :=
  93    (continuous_id.prodMk continuous_id).continuousOn
  94  have h_maps : Set.MapsTo (fun w : ℝ => ((w, w) : ℝ × ℝ))
  95      (Set.image F (Set.Ioi 0))
  96      ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := by
  97    intro w hw
  98    exact ⟨hw, hw⟩
  99  -- Use ContinuousOn.comp on the explicit lambda form of uncurry.
 100  have h_phi_on : ContinuousOn (fun p : ℝ × ℝ => Phi p.1 p.2)
 101      ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := hCont
 102  have h_comp : ContinuousOn
 103      ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘ (fun w : ℝ => ((w, w) : ℝ × ℝ)))
 104      (Set.image F (Set.Ioi 0)) :=