OAI/Analysis/HenonEmden/CapGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HenonLaneEmden.CapGeometry.band line 15

    Source documentation

    Radial bands in the positive-radius factor of polar coordinates.

    def band (a b : ℝ) : Set (Ioi (0:ℝ)) := {r | a < r.1 ∧ r.1 < b}
  2. lemma OAI.HenonLaneEmden.CapGeometry.volumeIoiPow_band_bounds line 17
  3. lemma OAI.HenonLaneEmden.CapGeometry.polar_rectangle_le line 45
  4. lemma OAI.HenonLaneEmden.CapGeometry.measure_le_polar_rectangle line 64
  5. lemma OAI.HenonLaneEmden.CapGeometry.norm_unit line 85
  6. lemma OAI.HenonLaneEmden.CapGeometry.polar_unit_distance line 89
  7. lemma OAI.HenonLaneEmden.CapGeometry.cap_lower_product line 105
  8. lemma OAI.HenonLaneEmden.CapGeometry.cap_upper_product line 135
  9. lemma OAI.HenonLaneEmden.CapGeometry.cap_real_bounds line 166
  10. lemma OAI.HenonLaneEmden.CapGeometry.cap_constants_pos line 218