OAI/Analysis/NodalLength/GridImprovement.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpNodal.Profiles.GridIndex line 135
  2. def OAI.SharpNodal.Profiles.gridCenter line 137
  3. def OAI.SharpNodal.Profiles.gridCenters line 140
  4. lemma OAI.SharpNodal.Profiles.gridCenter_coord line 142
  5. lemma OAI.SharpNodal.Profiles.gridCenter_norm line 155
  6. lemma OAI.SharpNodal.Profiles.fin_real_abs_sub_ge_one line 165
  7. lemma OAI.SharpNodal.Profiles.gridCenter_separated line 173
  8. lemma OAI.SharpNodal.Profiles.gridCenter_injective line 187
  9. lemma OAI.SharpNodal.Profiles.gridCenters_card line 194
  10. lemma OAI.SharpNodal.Profiles.gridCenters_norm line 198
  11. lemma OAI.SharpNodal.Profiles.gridCenters_separated line 203
  12. lemma OAI.SharpNodal.Profiles.gridCenters_card_identity line 210
  13. lemma OAI.SharpNodal.Profiles.profile_weighted_sup_real line 223
  14. def OAI.SharpNodal.Profiles.massExcess line 249
  15. lemma OAI.SharpNodal.Profiles.logRate_real line 251
  16. lemma OAI.SharpNodal.Profiles.massExcess_div line 257
  17. lemma OAI.SharpNodal.Profiles.eventual_massExcess_bound line 264
  18. lemma OAI.SharpNodal.Profiles.tiltedMass_mono_set line 287
  19. lemma OAI.SharpNodal.Profiles.profile_massExcess_transfer line 291
  20. lemma OAI.SharpNodal.Profiles.exists_fine_grid line 318
  21. lemma OAI.SharpNodal.Profiles.profile_affine_fixed_grid line 334
  22. lemma OAI.SharpNodal.Profiles.tiltedMass_const_mul line 373
  23. lemma OAI.SharpNodal.Profiles.massExcess_mul_left line 380
  24. lemma OAI.SharpNodal.Profiles.tiltedMass_normalized line 386
  25. lemma OAI.SharpNodal.Profiles.normalized_inner_rate line 397
  26. lemma OAI.SharpNodal.Profiles.profile_anchor_from_mass line 433
  27. lemma OAI.SharpNodal.Profiles.grid_child_closedBall_subset line 456
  28. lemma OAI.SharpNodal.Profiles.tilted_grid_averaged_transfer line 470
  29. def OAI.SharpNodal.Profiles.gridExcess line 535
  30. def OAI.SharpNodal.Profiles.gridMassesFinite line 542
  31. theorem OAI.SharpNodal.Profiles.sequence_affine_improvement line 549