OAI/Analysis/MumfordShah/Poincare.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah poincare.

  1. lemma OAI.MumfordShah.sq_integral_le_mass_mul_integral_sq line 23
  2. lemma OAI.MumfordShah.sq_sub_le_length_mul_integral_deriv_sq line 59
  3. lemma OAI.MumfordShah.sq_sub_mean_le_mean_sq_sub line 97
  4. lemma OAI.MumfordShah.square_path_estimate line 117
  5. def OAI.MumfordShah.coordSquare line 168
  6. lemma OAI.MumfordShah.isCompact_coordSquare line 170
  7. instance OAI.MumfordShah.coordSquare_finiteMeasure line 173
  8. lemma OAI.MumfordShah.mass_coordSquare line 177
  9. lemma OAI.MumfordShah.integral_square_fst line 184
  10. lemma OAI.MumfordShah.integral_square_snd line 191
  11. lemma OAI.MumfordShah.integral_square_rows line 198
  12. lemma OAI.MumfordShah.integral_square_cols line 207
  13. lemma OAI.MumfordShah.pointwise_sub_unitmean_sq_bound line 216
  14. lemma OAI.MumfordShah.unitmean_poincare_square line 273
  15. def OAI.MumfordShah.complexSquare line 306
  16. lemma OAI.MumfordShah.isCompact_complexSquare line 308
  17. instance OAI.MumfordShah.complexSquare_finiteMeasure line 311
  18. lemma OAI.MumfordShah.integral_complexSquare line 315
  19. lemma OAI.MumfordShah.norm_complexCoordInverse_le line 324
  20. lemma OAI.MumfordShah.coord_derivative_norm_le line 338
  21. lemma OAI.MumfordShah.unitmean_poincare_complexSquare line 355