OAI/Analysis/ProductSpaces/GaussianBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IndependentProducts.FiniteHead.affine_algebraic_tail line 13
  2. lemma OAI.IndependentProducts.averaged_midpoint_from_scalar line 39
  3. lemma OAI.IndependentProducts.gaussianSquareLaw_memLp line 66
  4. lemma OAI.IndependentProducts.gaussianSquareLaw_mean line 70
  5. lemma OAI.IndependentProducts.gaussianSquareLaw_second line 74
  6. lemma OAI.IndependentProducts.gaussianSquareLaw_hypotheses line 78
  7. lemma OAI.IndependentProducts.gaussian_midpoint_parameter line 98
  8. theorem OAI.IndependentProducts.main_gaussian_12 line 121

    Distinct definitions of this name: ComparatorChallenges/IndependentProducts.lean:109 (same statement text; different proof or body). Qualify references as OAI.IndependentProducts.main_gaussian_12@path.

  9. theorem OAI.IndependentProducts.main_gaussian_24 line 140

    Distinct definitions of this name: ComparatorChallenges/IndependentProducts.lean:102 (same statement text; different proof or body). Qualify references as OAI.IndependentProducts.main_gaussian_24@path.