OAI/Analysis/CircleDomains/Selection/ParallelLineIntegration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Integration of the parallel-line payments

The linewise variation and hole costs are integrated without a measurable choice of crossing segments. Cauchy–Schwarz is applied only to the density in the chosen bounded region. This is the integration step of the parallel-line lemma in Section 5 of the Koebe manuscript.

  1. theorem OAI.CircleDomainRigidity.integral_le_sqrt_measure_mul_L2 line 19
  2. theorem OAI.CircleDomainRigidity.integral_le_disk_L2 line 30
  3. theorem OAI.CircleDomainRigidity.integral_horizontal_slices line 54
  4. theorem OAI.CircleDomainRigidity.integrated_parallel_line_payment line 66
  5. theorem OAI.CircleDomainRigidity.integrated_parallel_line_payment_square_norm line 101