OAI/Analysis/CircleDomains/Probability/ContinuousMeasureModulus.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

An admissible bounded continuous real function bounds the pointwise modulus through its actual L² norm. Absolute values preserve admissibility.

  1. lemma OAI.CircleDomainRigidity.boundedContinuous_integral_sq_eq_norm_sq line 20
  2. lemma OAI.CircleDomainRigidity.measureFamilyModulus_le_boundedContinuous_norm line 34