OAI/Analysis/CircleDomains/Sobolev/PartitionMixing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Smooth mixing on an open planar domain. The locally finite sum is represented by an actual finite sum in a neighborhood of each point.

  1. def OAI.CircleDomainRigidity.OpenPlanePartition.mix line 20
  2. theorem OAI.CircleDomainRigidity.OpenPlanePartition.point_finite line 23
  3. theorem OAI.CircleDomainRigidity.OpenPlanePartition.mix_mem_Icc line 33
  4. theorem OAI.CircleDomainRigidity.OpenPlanePartition.eventually_finite_weights line 39
  5. theorem OAI.CircleDomainRigidity.OpenPlanePartition.mix_eventually_eq_sum line 55
  6. theorem OAI.CircleDomainRigidity.OpenPlanePartition.mix_contDiffOn line 68
  7. theorem OAI.CircleDomainRigidity.OpenPlanePartition.mix_fderiv line 77
  8. theorem OAI.CircleDomainRigidity.finite_partition_gradient_error line 109