OAI/Analysis/CircleDomains/Sobolev/MeasurableCircleGradient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The intrinsic circle differential is Borel measurable for a Borel circle coordinate. Two fixed cuts suffice on the continuity set; at a discontinuity every real branch is nondifferentiable and its derivative is zero. This supplies the actual gradient used in grid averaging.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.circleFDeriv_eq_fixed_cut line 17
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.circleFDeriv_eq_zero_of_not_continuousAt line 28
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.measurable_circleFDeriv line 37
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.measurable_circleGradient line 66