OAI/Analysis/StrictMeans/HorizontalLength.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.horizontalCutoff line 90
  2. lemma OAI.StrictInverseFirstPower.horizontalCutoff_zero line 93
  3. lemma OAI.StrictInverseFirstPower.horizontalCutoff_one line 100
  4. lemma OAI.StrictInverseFirstPower.horizontalCutoff_eq_nhds line 107
  5. lemma OAI.StrictInverseFirstPower.horizontalCutoff_contDiff line 114
  6. lemma OAI.StrictInverseFirstPower.horizontalCutoff_compact line 131
  7. lemma OAI.StrictInverseFirstPower.planeLaplacian_continuous line 152
  8. lemma OAI.StrictInverseFirstPower.planeLaplacian_compact line 157
  9. lemma OAI.StrictInverseFirstPower.holomorphic_integrable_image line 162
  10. lemma OAI.StrictInverseFirstPower.horizontal_smooth_green line 170
  11. lemma OAI.StrictInverseFirstPower.pullback_laplacian_integrable line 192
  12. lemma OAI.StrictInverseFirstPower.pullback_laplacian_integral_le line 202
  13. lemma OAI.StrictInverseFirstPower.horizontal_smooth_bound line 214
  14. lemma OAI.StrictInverseFirstPower.horizontal_smooth_integrable line 258
  15. lemma OAI.StrictInverseFirstPower.continuous_halfPlaneFunction_line line 280
  16. lemma OAI.StrictInverseFirstPower.compact_smooth_majorant line 291
  17. theorem OAI.StrictInverseFirstPower.horizontal_length_bound line 305