OAI/Analysis/KadisonKastler/StripBoundaryUniqueness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness from one boundary of a holomorphic strip

  1. def OAI.KadisonKastler.stripZeroExtension line 16
  2. theorem OAI.KadisonKastler.strip_eq_zero_of_lower_boundary line 20

    Source documentation

    A continuous holomorphic strip is determined by its lower boundary.

    theorem strip_eq_zero_of_lower_boundary {f : ℂ → ℂ}
    (hc : ContinuousOn f {z | 0 ≤ z.im ∧ z.im ≤ 1})
    (hd : DifferentiableOn ℂ f {z | 0 < z.im ∧ z.im < 1})
    (hzero : ∀ t : ℝ, f t = 0) :
    ∀ z : ℂ, 0 ≤ z.im → z.im ≤ 1 → f z = 0 := by
…
  3. theorem OAI.KadisonKastler.strip_eq_of_lower_boundary line 81