OAI/Analysis/CircleDomains/Sobolev/BoundedUpperIntegral.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Weak upper semicontinuity of integrals of bounded upper semicontinuous tests. For a test between zero and one, its integral is the product measure of its closed hypograph in the product with the unit interval. Thus the closed-set Portmanteau theorem suffices.

  1. def OAI.CircleDomainRigidity.unitIntervalProbability line 20
  2. theorem OAI.CircleDomainRigidity.hypograph_probability_eq_lintegral line 23
  3. theorem OAI.CircleDomainRigidity.upperSemicontinuous_integral_unit_bounded line 39
  4. theorem OAI.CircleDomainRigidity.upperSemicontinuous_integral_bounded line 69