OAI/Geometry/Perimeter/Regularity/SphericalFrankel.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RPISingularHarnack.SphericalFrankel.Frame line 11
  2. def OAI.RPISingularHarnack.SphericalFrankel.IsFrame line 13
  3. def OAI.RPISingularHarnack.SphericalFrankel.proj line 16
  4. def OAI.RPISingularHarnack.SphericalFrankel.angle line 19
  5. def OAI.RPISingularHarnack.SphericalFrankel.defect line 21
  6. def OAI.RPISingularHarnack.SphericalFrankel.traceProduct line 23
  7. def OAI.RPISingularHarnack.SphericalFrankel.cross line 27
  8. lemma OAI.RPISingularHarnack.SphericalFrankel.proj_inner_self line 29
  9. lemma OAI.RPISingularHarnack.SphericalFrankel.defect_eq line 40
  10. lemma OAI.RPISingularHarnack.SphericalFrankel.cross_eq line 45
  11. lemma OAI.RPISingularHarnack.SphericalFrankel.cross_abs_le line 57
  12. lemma OAI.RPISingularHarnack.SphericalFrankel.angle_abs_le_one line 63
  13. lemma OAI.RPISingularHarnack.SphericalFrankel.traceProduct_eq line 67
  14. lemma OAI.RPISingularHarnack.SphericalFrankel.scalar_gap_bound line 76
  15. lemma OAI.RPISingularHarnack.SphericalFrankel.traceProduct_lower_bound line 141
  16. lemma OAI.RPISingularHarnack.SphericalFrankel.continuous_proj line 169
  17. lemma OAI.RPISingularHarnack.SphericalFrankel.continuous_angle line 173
  18. lemma OAI.RPISingularHarnack.SphericalFrankel.continuous_defect line 177
  19. lemma OAI.RPISingularHarnack.SphericalFrankel.continuous_traceProduct line 181
  20. lemma OAI.RPISingularHarnack.SphericalFrankel.continuous_cross line 186
  21. lemma OAI.RPISingularHarnack.SphericalFrankel.isClosed_frames line 190
  22. lemma OAI.RPISingularHarnack.SphericalFrankel.isCompact_frames line 197
  23. lemma OAI.RPISingularHarnack.SphericalFrankel.integrable_pairFrameFunction line 202
  24. def OAI.RPISingularHarnack.SphericalFrankel.angularWeight line 211
  25. lemma OAI.RPISingularHarnack.SphericalFrankel.angularWeight_contDiff line 213
  26. lemma OAI.RPISingularHarnack.SphericalFrankel.angularWeight_nonneg line 216
  27. lemma OAI.RPISingularHarnack.SphericalFrankel.angularWeight_pos_iff line 219
  28. lemma OAI.RPISingularHarnack.SphericalFrankel.angularWeight_zero_of_nonpos line 228
  29. lemma OAI.RPISingularHarnack.SphericalFrankel.angularWeight_hasDerivAt line 231
  30. lemma OAI.RPISingularHarnack.SphericalFrankel.angularWeight_deriv line 244
  31. lemma OAI.RPISingularHarnack.SphericalFrankel.angularWeight_deriv_lower line 248
  32. lemma OAI.RPISingularHarnack.SphericalFrankel.angularWeight_deriv_nonneg line 253
  33. structure OAI.RPISingularHarnack.SphericalFrankel.CoupledStationarity line 257
  34. lemma OAI.RPISingularHarnack.SphericalFrankel.continuous_defect_sum line 267
  35. lemma OAI.RPISingularHarnack.SphericalFrankel.angularWeight_integral_pos line 273
  36. lemma OAI.RPISingularHarnack.SphericalFrankel.weighted_trace_lower_bound line 335
  37. theorem OAI.RPISingularHarnack.SphericalFrankel.no_positive_angle_gap line 351