OAI/Analysis/NodalLength/ProfileExtraction.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpNodal.Profiles.basisProfile line 29
  2. lemma OAI.SharpNodal.Profiles.basisProfile_le line 32
  3. lemma OAI.SharpNodal.Profiles.basisProfile_lt_iff line 36
  4. lemma OAI.SharpNodal.Profiles.upperSemicontinuous_basisProfile line 40
  5. lemma OAI.SharpNodal.Profiles.basisProfile_nonpos line 47
  6. theorem OAI.SharpNodal.Profiles.extract_basis_rates line 53
  7. lemma OAI.SharpNodal.Profiles.basis_rates_nonpos line 63
  8. lemma OAI.SharpNodal.Profiles.open_profile_lower line 76
  9. lemma OAI.SharpNodal.Profiles.compact_profile_upper line 93
  10. lemma OAI.SharpNodal.Profiles.upper_test_of_maximum line 149
  11. lemma OAI.SharpNodal.Profiles.negative_trace_coordinate line 165
  12. theorem OAI.SharpNodal.Profiles.full_test_of_nonexceptional line 171
  13. lemma OAI.SharpNodal.Profiles.ereal_add_coe_lt_coe_iff line 306
  14. lemma OAI.SharpNodal.Profiles.ereal_coe_lt_add_coe_iff line 319
  15. def OAI.SharpNodal.Profiles.weightedMass line 335
  16. lemma OAI.SharpNodal.Profiles.weightedMass_mono_set line 339
  17. lemma OAI.SharpNodal.Profiles.weightedMass_upper line 344
  18. lemma OAI.SharpNodal.Profiles.weightedMass_lower line 354
  19. lemma OAI.SharpNodal.Profiles.weightedMass_biUnion_le line 363
  20. lemma OAI.SharpNodal.Profiles.basis_rates_mono line 375
  21. theorem OAI.SharpNodal.Profiles.weighted_compact_profile_upper line 385
  22. theorem OAI.SharpNodal.Profiles.weighted_open_profile_lower line 450
  23. def OAI.SharpNodal.Profiles.tiltedDensity line 494
  24. def OAI.SharpNodal.Profiles.tiltedMeasure line 497
  25. lemma OAI.SharpNodal.Profiles.continuousOn_tiltedDensity line 500
  26. lemma OAI.SharpNodal.Profiles.tiltedDensity_weight line 506
  27. lemma OAI.SharpNodal.Profiles.weightedMass_tiltedMeasure line 521
  28. theorem OAI.SharpNodal.Profiles.extract_tilted_profile line 532
  29. def OAI.SharpNodal.Profiles.ShiftedTestProperty line 574
  30. theorem OAI.SharpNodal.Profiles.shifted_test_of_profile line 578
  31. lemma OAI.SharpNodal.Profiles.gradient_sub_linear line 609
  32. lemma OAI.SharpNodal.Profiles.laplacian_sub_linear line 615
  33. lemma OAI.SharpNodal.Profiles.upperTest_sub_real line 625
  34. lemma OAI.SharpNodal.Profiles.upperTest_add_real line 638
  35. theorem OAI.SharpNodal.Profiles.full_test_of_shifted line 648