OAI/Analysis/HenonEmden/Components.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HenonLaneEmden.LineComponents.SegmentInside line 17

   Source documentation

   All points of the closed segment between the base point 0 and r remain in the open line layer.

   def SegmentInside (U : Set (X × ℝ)) (p : X) (r : ℝ) : Prop :=
   …

2. lemma OAI.HenonLaneEmden.LineComponents.segmentInside_iff_mem_component line 21
3. lemma OAI.HenonLaneEmden.LineComponents.segmentInside_zero line 33
4. lemma OAI.HenonLaneEmden.LineComponents.segmentInside_base line 37
5. lemma OAI.HenonLaneEmden.LineComponents.segmentInside_endpoint line 41
6. lemma OAI.HenonLaneEmden.LineComponents.isOpen_segmentInside line 44
7. lemma OAI.HenonLaneEmden.LineComponents.isOpen_section line 57
8. def OAI.HenonLaneEmden.LineComponents.forwardExit line 62

   Source documentation

   The rational definition makes joint measurability independent of coordinates on the direction-dependent transverse hyperplanes.

   noncomputable def forwardExit (U : Set (X × ℝ)) (p : X) : ℝ≥0∞ :=
   …

9. def OAI.HenonLaneEmden.LineComponents.backwardExit line 65
10. def OAI.HenonLaneEmden.LineComponents.componentLength line 68
11. def OAI.HenonLaneEmden.LineComponents.componentInf line 71
12. lemma OAI.HenonLaneEmden.LineComponents.componentInf_le_base line 75
13. lemma OAI.HenonLaneEmden.LineComponents.componentInf_ne_top line 82
14. def OAI.HenonLaneEmden.LineComponents.componentWeight line 86
15. lemma OAI.HenonLaneEmden.LineComponents.componentWeight_le_base line 93
16. lemma OAI.HenonLaneEmden.LineComponents.componentInf_eq_component line 101

    Source documentation

    The rational infimum equals the infimum over the genuine open component.

    lemma componentInf_eq_component {U : Set (X × ℝ)} (hU : IsOpen U)
        {value : X × ℝ → ℝ} {p : X} (hp : (p,0) ∈ U)
        (hv : Continuous (fun s : ℝ => value (p,s))) :
        componentInf U value p =
          ⨅ s ∈ connectedComponentIn {s : ℝ | (p,s) ∈ U} 0, ENNReal.ofReal (value (p,s)) := by
    …

    Mentions: OAI.HenonLaneEmden.LineComponents.componentInf

17. lemma OAI.HenonLaneEmden.LineComponents.lt_forwardExit_iff line 133

    Source documentation

    Exceeding a nonnegative forward offset is precisely the compact-segment condition. Openness is needed to replace membership of the endpoint by strict inequality of the exit distance.

    lemma lt_forwardExit_iff {U : Set (X × ℝ)} (hU : IsOpen U) {p : X} {r : ℝ}
        (hr : 0 ≤ r) : ENNReal.ofReal r < forwardExit U p ↔ SegmentInside U p r := by
    …

    Mentions: OAI.HenonLaneEmden.LineComponents.forwardExit, OAI.HenonLaneEmden.LineComponents.SegmentInside

18. lemma OAI.HenonLaneEmden.LineComponents.segmentInside_reflect line 159
19. lemma OAI.HenonLaneEmden.LineComponents.lt_backwardExit_iff line 175
20. lemma OAI.HenonLaneEmden.LineComponents.forwardExit_pos line 183
21. lemma OAI.HenonLaneEmden.LineComponents.backwardExit_pos line 188
22. lemma OAI.HenonLaneEmden.LineComponents.component_eq_Ioo line 193
23. lemma OAI.HenonLaneEmden.LineComponents.volume_component line 212
24. lemma OAI.HenonLaneEmden.LineComponents.measurable_forwardExit line 227
25. lemma OAI.HenonLaneEmden.LineComponents.measurable_backwardExit line 233
26. lemma OAI.HenonLaneEmden.LineComponents.measurable_componentLength line 239
27. lemma OAI.HenonLaneEmden.LineComponents.measurable_componentInf line 243
28. lemma OAI.HenonLaneEmden.LineComponents.measurable_componentWeight line 250