OnePointPickPositive

formal source

  87
  88/-- One-point Pick positivity. This is the `N = 1` principal minor of the
  89full Pick matrix. -/
  90def OnePointPickPositive (chart : HalfStripDiskChart)
  91    (X : XiCayleyField) : Prop :=
  92  ∀ s : ℂ, RightHalfStrip s →
  93    0 ≤ (1 - ‖X s‖ ^ 2) / (1 - ‖chart.φ s‖ ^ 2)
  94
  95/-- Full finite Pick positivity, stated as an interface. The one-point field is
  96included explicitly because it is the part we use theorem-grade here. -/
  97structure FinitePickPositive (chart : HalfStripDiskChart)
  98    (X : XiCayleyField) : Prop where
  99  one_point : OnePointPickPositive chart X
 100  finite_matrices_positive : True
 101
 102/-- The Schur bound on the right half-strip. -/
 103def SchurOnRightHalfStrip (X : XiCayleyField) : Prop :=
 104  ∀ s : ℂ, RightHalfStrip s → ‖X s‖ ≤ 1
 105
 106/-- One-point Pick positivity forces the pointwise Schur bound. -/
 107theorem schur_of_onePointPickPositive
 108    (chart : HalfStripDiskChart) (X : XiCayleyField)
 109    (hpick : OnePointPickPositive chart X) :
 110    SchurOnRightHalfStrip X := by
 111  intro s hs
 112  have hden_pos : 0 < 1 - ‖chart.φ s‖ ^ 2 := by
 113    have hφ : ‖chart.φ s‖ < 1 := chart.maps_to_disk s hs
 114    have hφ_nonneg : 0 ≤ ‖chart.φ s‖ := norm_nonneg _
 115    nlinarith
 116  have hfrac : 0 ≤ (1 - ‖X s‖ ^ 2) / (1 - ‖chart.φ s‖ ^ 2) :=
 117    hpick s hs
 118  have hnum_nonneg : 0 ≤ 1 - ‖X s‖ ^ 2 := by
 119    have hmul :
 120        0 ≤ ((1 - ‖X s‖ ^ 2) / (1 - ‖chart.φ s‖ ^ 2)) *