More work + cleanup

BonnAnalysis/ComplexInterpolation.lean

@@ -3,6 +3,7 @@ import Mathlib.Order.Filter.Basic
 import BonnAnalysis.Dual
 import Mathlib.Topology.MetricSpace.Sequences
 import Mathlib.Analysis.Complex.HalfPlane
+import Mathlib.Analysis.Complex.ReImTopology
 
 noncomputable section
 
@@ -27,7 +28,7 @@ variable {α β E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {n : Measurab
 /- TODO: split proofs into smaller lemmas to recycle code -/
 
 -- All these names are probably very bad
-lemma real_pow_le_pow_iff {M:ℝ} (hM: M>0) (a b : ℝ) : M^a ≤ M^b ↔ ((1 ≤ M ∧ a ≤ b ) ∨ (M ≤ 1 ∧ b ≤ a)) := by{
+lemma Real.pow_le_pow_iff {M:ℝ} (hM: M>0) (a b : ℝ) : M^a ≤ M^b ↔ ((1 ≤ M ∧ a ≤ b ) ∨ (M ≤ 1 ∧ b ≤ a)) := by{
   have hMb : M^(-b) > 0 := Real.rpow_pos_of_pos hM (-b)
   rw[← mul_le_mul_right hMb, ←Real.rpow_add, ← Real.rpow_add]
   simp
@@ -46,7 +47,7 @@ lemma pow_bound₀ {M:ℝ} (hM: M > 0) {z: ℂ} (hz: z.re ∈ Icc 0 1) : Complex
   · left
     have : 1 = M^0 := rfl
     nth_rewrite 2 [this]
-    have := (real_pow_le_pow_iff hM (z.re-1) 0).mpr
+    have := (Real.pow_le_pow_iff hM (z.re-1) 0).mpr
     simp at this
     apply this
     left
@@ -56,7 +57,7 @@ lemma pow_bound₀ {M:ℝ} (hM: M > 0) {z: ℂ} (hz: z.re ∈ Icc 0 1) : Complex
   · right
     have : M^(-1:ℝ) = M⁻¹ := by apply Real.rpow_neg_one
     rw[← this]
-    have := (real_pow_le_pow_iff hM (z.re-1) (-1:ℝ)).mpr
+    have := (Real.pow_le_pow_iff hM (z.re-1) (-1:ℝ)).mpr
     simp at this
     apply this
     right
@@ -74,7 +75,7 @@ lemma pow_bound₁ {M:ℝ} (hM: M > 0) {z: ℂ} (hz: z.re ∈ Icc 0 1) : Complex
   · left
     have : 1 = M^0 := rfl
     rw [this]
-    have := (real_pow_le_pow_iff hM (-z.re) 0).mpr
+    have := (Real.pow_le_pow_iff hM (-z.re) 0).mpr
     simp at this
     apply this
     left
@@ -84,7 +85,7 @@ lemma pow_bound₁ {M:ℝ} (hM: M > 0) {z: ℂ} (hz: z.re ∈ Icc 0 1) : Complex
   · right
     have : M^(-1:ℝ) = M⁻¹ := by apply Real.rpow_neg_one
     rw[← this]
-    have := (real_pow_le_pow_iff hM (-z.re) (-1:ℝ)).mpr
+    have := (Real.pow_le_pow_iff hM (-z.re) (-1:ℝ)).mpr
     simp at this
     apply this
     right
@@ -130,30 +131,42 @@ lemma abs_fun_bounded {f:ℂ → ℂ} (h2f : IsBounded (f '' { z | z.re ∈ Icc
 #check Complex.norm_eqOn_closure_of_isPreconnected_of_isMaxOn -- I believe this is the one!
 
 
-#check IsPreconnected.image
-
-#check IsPreconnected.prod --but this would require seeing ℂ as ℝ^2
-
 /- Some technical lemmas to apply the maximum modulus principle -/
-lemma isPreconnected_strip : IsPreconnected { z : ℂ | z.re ∈ Ioo 0 1} := by{
-  sorry
+lemma strip_prod : { z:ℂ  | z.re ∈ Ioo 0 1} = (Ioo 0 1 : Set ℝ) ×ℂ univ := by{
+  ext z
+  simp[Complex.mem_reProdIm]
 }
 
-lemma isOpen_strip : IsOpen { z : ℂ | z.re ∈ Ioo 0 1} := by{
-  simp
-  have : {z:ℂ  | 0 < z.re ∧ z.re < 1} = {z | (z.re: EReal) < 1} ∩ {z | 0 < (z.re: EReal) } := by {
-    simp
-    norm_cast
+lemma clstrip_prod : {z: ℂ | z.re ∈ Icc 0 1} = (Icc 0 1 : Set ℝ) ×ℂ univ := by{
+  ext z
+  simp[Complex.mem_reProdIm]
+}
+
+
+lemma isPreconnected_strip : IsPreconnected { z : ℂ | z.re ∈ Ioo 0 1} := by{
+  have : { z : ℂ | z.re ∈ Ioo 0 1} = ⇑equivRealProdCLM.toHomeomorph ⁻¹' ((Ioo 0 1 : Set ℝ) ×ˢ  (univ: Set ℝ)) := by{
     ext z
     simp
-    tauto
   }
-  rw[this]
-  apply IsOpen.inter (Complex.isOpen_re_lt_EReal 1) (Complex.isOpen_re_gt_EReal 0)
+  rw[this, Homeomorph.isPreconnected_preimage Complex.equivRealProdCLM.toHomeomorph]
+  exact IsPreconnected.prod isPreconnected_Ioo isPreconnected_univ
+}
+
+lemma isOpen_strip : IsOpen { z : ℂ | z.re ∈ Ioo 0 1} := by{
+  rw[strip_prod]
+  exact IsOpen.reProdIm isOpen_Ioo isOpen_univ
 }
 
+lemma isClosed_clstrip : IsClosed { z : ℂ | z.re ∈ Icc 0 1} := by{
+  rw[clstrip_prod]
+  exact IsClosed.reProdIm isClosed_Icc isClosed_univ
+}
+
+
 lemma closure_strip : closure { z:ℂ  | z.re ∈ Ioo 0 1} = { z: ℂ  | z.re ∈ Icc 0 1} := by{
-  sorry
+  rw[strip_prod, clstrip_prod]
+  rw [Complex.closure_reProdIm, closure_univ, closure_Ioo]
+  norm_num
 }
 
 /-- Hadamard's three lines lemma/theorem on the unit strip with bounds M₀=M₁=1 and vanishing at infinity condition. -/
@@ -178,10 +191,28 @@ theorem DiffContOnCl.norm_le_pow_mul_pow''' {f : ℂ → ℂ}
       obtain ⟨z, hz⟩ := Classical.axiom_of_choice hu3
       let S := {w | (0 ≤ w.re ∧ w.re ≤ 1) ∧ ∃ n : ℕ, Complex.abs (f w) = u n}
       have hS : IsBounded S := by{
+        -- here, we use the vanishing at infinity
+        -- I guess morally the idea is that it is contained in a rectangle
+        -- but we need to use the 'eventually' in hu2
+
+
+        -- #check Bornology.IsBounded.reProdIm
         sorry
 
       }
 
+      have hS' : S ⊆  {w | (0 ≤ w.re ∧ w.re ≤ 1)} := by{
+        simp[S]
+        intros
+        tauto
+      }
+
+      have hSclos : closure S ⊆ {w | (0 ≤ w.re ∧ w.re ≤ 1)} := by{
+        apply (IsClosed.closure_subset_iff isClosed_clstrip).mpr
+        simp
+        exact hS'
+      }
+
       have hzS : ∀ n : ℕ, z n ∈ S := by{
         intro n
         simp[S]
@@ -193,13 +224,16 @@ theorem DiffContOnCl.norm_le_pow_mul_pow''' {f : ℂ → ℂ}
 
       obtain ⟨z',hz', φ, hφ₁, hφ₂⟩ := tendsto_subseq_of_bounded hS hzS
 
-      --I may not even need this one
       have hmax : IsMaxOn (norm ∘ f) { w:ℂ  | w.re ∈ Icc 0 1} z' := by{
         sorry
       }
 
-      --This one I do need
+
       have hmax' : IsMaxOn (norm ∘ f) { w:ℂ  | w.re ∈ Ioo 0 1} z' := by{
+        simp[IsMaxOn, IsMaxFilter]
+        intro w hw₁ hw₂
+        -- I want to say: find n with Complex.abs (f (u n)) ≥  Complex.abs (f w)
+        --simp[Tendsto, map, atTop, nhds] at hu2
         sorry
       }
 
@@ -231,7 +265,17 @@ theorem DiffContOnCl.norm_le_pow_mul_pow''' {f : ℂ → ℂ}
         exact h₀f
 
       · have : z'.re = 0 ∨ z'.re = 1 := by{
-          sorry
+          simp at h
+          have : z'.re ≥ 0 ∧ z'.re ≤ 1 := by{
+            specialize hSclos hz'
+            simp at hSclos
+            tauto
+          }
+          by_cases hc: z'.re = 0
+          · left; assumption
+          · right
+            specialize h (lt_of_le_of_ne this.1 (Ne.symm hc) )
+            exact eq_of_le_of_le this.2 h
         }
         simp[IsMaxOn, IsMaxFilter] at hmax
         specialize hmax (t+I*y)