OAI/Probability/SLE/Mass/SimultaneousConvexTails.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The countable deterministic extraction in mass:construction. A weighted Hilbert sum ensures the same finite convex coefficients work for every member of the countable family of bounded test sequences.

  1. lemma OAI.SLEExactGauge.geometric_half_mem_l2 line 18
  2. theorem OAI.SLEExactGauge.exists_simultaneous_convex_tail_combinations line 28