OAI/Analysis/CircleDomains/Probability/ProbabilitySquareBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Squared density and finite visit bounds survive probability mixtures. These estimates allow the fused law to retain the original quantitative bounds.

  1. theorem OAI.CircleDomainRigidity.sq_lintegral_le_lintegral_sq_of_probability line 17
  2. theorem OAI.CircleDomainRigidity.finite_square_moment_mixture_bound line 29
  3. theorem OAI.CircleDomainRigidity.density_square_integral_mixture_bound line 41