ComplexBall.lean

1import BFPP.Necessity2import Mathlib.Analysis.Complex.Basic34/-! # The real construction also yields a map on the complex unit ball -/56namespace BFPP78set_option autoImplicit false910universe u11variable {K : Type u} [TopologicalSpace K] [CompactSpace K]1213noncomputable def ballRealPart (f : UnitBall C(K, ℂ)) : UnitBall C(K, ℝ) :=14  ⟨⟨fun t => (f.val t).re, Complex.continuous_re.comp f.val.continuous⟩, by15    apply (ContinuousMap.norm_le _ (by norm_num : (0 : ℝ) ≤ 1)).mpr16    intro t17    change |(f.val t).re| ≤ 118    exact (Complex.abs_re_le_norm _).trans ((f.val.norm_coe_le_norm t).trans f.property)⟩1920noncomputable def ballComplexify (f : UnitBall C(K, ℝ)) : UnitBall C(K, ℂ) :=21  ⟨⟨fun t => (f.val t : ℂ), Complex.continuous_ofReal.comp f.val.continuous⟩, by22    apply (ContinuousMap.norm_le _ (by norm_num : (0 : ℝ) ≤ 1)).mpr23    intro t24    change ‖(f.val t : ℂ)‖ ≤ 125    rw [Complex.norm_real]26    exact (f.val.norm_coe_le_norm t).trans f.property⟩2728@[simp] theorem ballRealPart_complexify (f : UnitBall C(K, ℝ)) :29    ballRealPart (ballComplexify f) = f := by30  apply Subtype.ext31  ext t32  rfl3334theorem ballRealPart_nonexpansive : LipschitzWith 1 (@ballRealPart K _ _) := by35  apply LipschitzWith.of_dist_le_mul36  intro f g37  simp only [NNReal.coe_one, one_mul]38  change dist (ballRealPart f).val (ballRealPart g).val ≤ dist f.val g.val39  rw [dist_eq_norm]40  apply (ContinuousMap.norm_le _ dist_nonneg).mpr41  intro t42  change ‖(f.val t).re - (g.val t).re‖ ≤ dist f.val g.val43  rw [dist_eq_norm]44  rw [← Complex.sub_re, Real.norm_eq_abs]45  exact (Complex.abs_re_le_norm _).trans ((f.val - g.val).norm_coe_le_norm t)4647theorem ballComplexify_nonexpansive : LipschitzWith 1 (@ballComplexify K _ _) := by48  apply LipschitzWith.of_dist_le_mul49  intro f g50  simp only [NNReal.coe_one, one_mul]51  change dist (ballComplexify f).val (ballComplexify g).val ≤ dist f.val g.val52  rw [dist_eq_norm]53  apply (ContinuousMap.norm_le _ dist_nonneg).mpr54  intro t55  change ‖(f.val t : ℂ) - (g.val t : ℂ)‖ ≤ dist f.val g.val56  rw [dist_eq_norm]57  rw [← Complex.ofReal_sub, Complex.norm_real]58  exact (f.val - g.val).norm_coe_le_norm t5960theorem complex_fixedPointFree_of_real61    (T : UnitBall C(K, ℝ) → UnitBall C(K, ℝ)) (hT : LipschitzWith 1 T)62    (hfree : ∀ f, T f ≠ f) :63    ∃ S : UnitBall C(K, ℂ) → UnitBall C(K, ℂ), LipschitzWith 1 S ∧ ∀ f, S f ≠ f := by64  refine ⟨fun f => ballComplexify (T (ballRealPart f)),65    nonexpansive_transfer ballRealPart ballComplexify T ballRealPart_nonexpansive66      ballComplexify_nonexpansive hT, ?_⟩67  intro f hf68  have h := congrArg ballRealPart hf69  exact hfree (ballRealPart f) (by simpa only [ballRealPart_complexify] using h)7071theorem exists_complex_fixedPointFree_of_not_ED [T2Space K] (hK : ¬ ExtremallyDisconnected K) :72    ∃ S : UnitBall C(K, ℂ) → UnitBall C(K, ℂ), LipschitzWith 1 S ∧ ∀ f, S f ≠ f := by73  obtain ⟨T, hT, hfree⟩ := exists_nonexpansive_fixedPointFree_of_not_ED hK74  exact complex_fixedPointFree_of_real T hT hfree7576end BFPP

SHA-256