OAI/Analysis/HenonEmden/Endpoints.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HenonLaneEmden.LineComponents.lowerEndpoint line 16

    Source documentation

    Relative endpoints are chosen by measurable rational exits. On the only components whose weight is positive they are the genuine finite endpoints.

    noncomputable def lowerEndpoint {P : Type uP} (U : Set (P × ℝ)) (p : P × ℝ) : ℝ :=
…
  2. def OAI.HenonLaneEmden.LineComponents.upperEndpoint line 18
  3. lemma OAI.HenonLaneEmden.LineComponents.measurable_lowerEndpoint line 21
  4. lemma OAI.HenonLaneEmden.LineComponents.measurable_upperEndpoint line 24
  5. lemma OAI.HenonLaneEmden.LineComponents.relative_component_eq_Ioo line 28
  6. lemma OAI.HenonLaneEmden.LineComponents.relative_endpoints_eq line 49
  7. lemma OAI.HenonLaneEmden.LineComponents.closure_component_inter_subset line 61

    Source documentation

    Components are closed relative to the original set.

    lemma closure_component_inter_subset {U : Set ℝ} {x : ℝ} (hx : x ∈ U) :
    closure (connectedComponentIn U x) ∩ U ⊆ connectedComponentIn U x := by
…
  8. lemma OAI.HenonLaneEmden.LineComponents.component_endpoints_frontier line 72
  9. lemma OAI.HenonLaneEmden.LineComponents.value_eq_level_at_endpoint line 94
  10. lemma OAI.HenonLaneEmden.LineComponents.setWeight_le_on_closure line 119
  11. lemma OAI.HenonLaneEmden.LineComponents.endpoints_distance_bound line 128
  12. lemma OAI.HenonLaneEmden.LineComponents.relative_componentLength_eq line 146
  13. lemma OAI.HenonLaneEmden.LineComponents.relative_endpoints_eq_of_weight_pos line 154