OAI/Geometry/Riemannian/HarmonicCore/InteriorBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_cutoff_sup_H1 line 18
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.cutoffSobolev_derivative_coe line 78
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coefficient_inner_integral line 88
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_cutoff_restrict line 98
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.cutoff_H1_L2_bound line 123
  6. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_cutoff_sup_L2 line 145
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.smooth_ball_cutoff line 187
  8. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_interior_sup_L2 line 210
  9. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.energyOperator_contDiff line 239
  10. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.compact_coefficient_bounds line 244
  11. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.convex_coefficient_coercive line 253
  12. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.bump_coefficient_coercive line 271
  13. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.smooth_energy_extension line 285
  14. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coefficient_ball_energy_eq line 312
  15. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_weak_interior_sup_L2 line 326