OAI/Analysis/AffineBernstein/VarianceSeparation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AffineBernstein.variance_lower_of_separated_sets line 16
  2. lemma OAI.AffineBernstein.compact_sublevel_in_compact line 51