OAI/Analysis/Conductivity/Sobolev/CentralPoincare.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.centralTop_subset_anchor line 11
  2. lemma OAI.ScalarConductivity.centralBottom_subset_anchor line 16
  3. lemma OAI.ScalarConductivity.centralColumn_overlaps_anchor line 21
  4. def OAI.ScalarConductivity.centralColumnConstant line 39
  5. lemma OAI.ScalarConductivity.centralColumnConstant_nonneg line 44
  6. lemma OAI.ScalarConductivity.centralColumn_poincare line 50
  7. lemma OAI.ScalarConductivity.localVariance_finset_union_le line 80
  8. def OAI.ScalarConductivity.centralPoincareConstant line 95
  9. lemma OAI.ScalarConductivity.centralPoincareConstant_nonneg line 98
  10. theorem OAI.ScalarConductivity.central_physical_poincare line 103
  11. def OAI.ScalarConductivity.centralMeasure line 144
  12. instance OAI.ScalarConductivity.centralMeasure_finite line 146
  13. def OAI.ScalarConductivity.centralSmoothFunctions line 150
  14. instance OAI.ScalarConductivity.(instance at line 160) line 160
  15. lemma OAI.ScalarConductivity.central_smooth line 162
  16. abbrev OAI.ScalarConductivity.CentralL2 line 164
  17. abbrev OAI.ScalarConductivity.CentralJets line 165
  18. abbrev OAI.ScalarConductivity.CentralGradients line 166
  19. lemma OAI.ScalarConductivity.central_continuous_memLp line 168
  20. def OAI.ScalarConductivity.centralJetField line 172
  21. lemma OAI.ScalarConductivity.centralJetField_continuous line 175
  22. def OAI.ScalarConductivity.centralSmoothJet line 183
  23. lemma OAI.ScalarConductivity.centralSmoothJet_ae line 186
  24. lemma OAI.ScalarConductivity.centralJetField_add line 189
  25. lemma OAI.ScalarConductivity.centralJetField_smul line 203
  26. def OAI.ScalarConductivity.centralSmoothJetL line 217
  27. def OAI.ScalarConductivity.centralJetD line 238
  28. lemma OAI.ScalarConductivity.centralSmoothJet_norm_coordinate line 242
  29. lemma OAI.ScalarConductivity.centralSmoothJet_gradient_norm line 249
  30. lemma OAI.ScalarConductivity.centralSmoothJet_norm line 267