OAI/Analysis/CircleDomains/Topology/QuarterCircleSubstitution.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Monotone one-dimensional substitutions for quarter-circle projections. The scalar integrand may be measurable rather than continuous.

  1. theorem OAI.CircleDomainRigidity.integral_quarter_sin line 12
  2. theorem OAI.CircleDomainRigidity.integral_quarter_cos line 26
  3. theorem OAI.CircleDomainRigidity.quarter_sin_sqrt line 43
  4. theorem OAI.CircleDomainRigidity.quarter_cos_sqrt line 50