feat(InputOutput): prove isGraph_inputOutput and isGraph_inputState

DynamicalSystems/InputOutput/ClosedLoop.lean

@@ -279,11 +279,68 @@ theorem comp_inputStateLp_mapProdLp (hG₁ : Function.graph G₁ = loop.topRel)
 
 end mem_loop
 
-proof_wanted isGraph_inputOutput (h_topRel : loop.topRel.IsGraph) (h_botRel : loop.botRel.IsGraph)
-    (h : loop.inputState.IsGraph) : loop.inputOutput.IsGraph
-
-proof_wanted isGraph_inputState (h_topRel : loop.topRel.IsGraph) (h_botRel : loop.botRel.IsGraph)
-    (h : loop.inputOutput.IsGraph) : loop.inputState.IsGraph
+/-- If the map from inputs to states is a graph, then the map from inputs to outputs is also a
+graph. -/
+theorem isGraph_inputOutput (_h_topRel : loop.topRel.IsGraph) (_h_botRel : loop.botRel.IsGraph)
+    (h : loop.inputState.IsGraph) : loop.inputOutput.IsGraph := by
+  intro e
+  obtain ⟨u, hu, hu_uniq⟩ := h e
+  refine ⟨fun a ↦ ((u a).2 - (e a).2, (e a).1 - (u a).1), ?_, ?_⟩
+  · dsimp only
+    rw [mem_inputOutput]
+    constructor
+    · convert hu.1 using 2
+      · ext a; simp
+      · ext a; simp
+    · convert hu.2 using 2
+      · ext a; simp
+      · ext a; simp
+  · intro y' hy'
+    have hu' := mem_inputState_of_mem_inputOutput hy'
+    have heq := hu_uniq _ hu'
+    ext a
+    · have h2 : (e - (fun x ↦ (x.2, -x.1)) ∘ y') a = u a := by rw [heq]
+      simp only [Pi.sub_apply, Function.comp_apply] at h2
+      have h2_snd := congr_arg Prod.snd h2
+      dsimp at h2_snd
+      rw [← h2_snd]
+      simp
+    · have h1 : (e - (fun x ↦ (x.2, -x.1)) ∘ y') a = u a := by rw [heq]
+      simp only [Pi.sub_apply, Function.comp_apply] at h1
+      have h1_fst := congr_arg Prod.fst h1
+      dsimp at h1_fst
+      rw [← h1_fst]
+      simp
+
+/-- If the map from inputs to outputs is a graph, then the map from inputs to states is also a
+graph. -/
+theorem isGraph_inputState (_h_topRel : loop.topRel.IsGraph) (_h_botRel : loop.botRel.IsGraph)
+    (h : loop.inputOutput.IsGraph) : loop.inputState.IsGraph := by
+  intro e
+  obtain ⟨y, hy, hy_uniq⟩ := h e
+  refine ⟨e - (fun x ↦ (x.2, -x.1)) ∘ y, mem_inputState_of_mem_inputOutput hy, ?_⟩
+  intro u' hu'
+  have hy' : (e, fun a ↦ ((u' a).2 - (e a).2, (e a).1 - (u' a).1)) ∈ loop.inputOutput := by
+    rw [mem_inputOutput]
+    constructor
+    · convert hu'.1 using 2
+      · ext a; simp
+      · ext a; simp
+    · convert hu'.2 using 2
+      · ext a; simp
+      · ext a; simp
+  have heq := hy_uniq _ hy'
+  ext a
+  · have h1 := congr_arg Prod.snd (congr_fun heq a)
+    dsimp at h1
+    simp only [Pi.sub_apply, Function.comp_apply, Prod.fst_sub]
+    rw [← h1]
+    simp
+  · have h2 := congr_arg Prod.fst (congr_fun heq a)
+    dsimp at h2
+    simp only [Pi.sub_apply, Function.comp_apply, Prod.snd_sub]
+    rw [← h2]
+    simp
 
 variable [MeasurableSpace α] {μ : Measure α}