OAI/Analysis/HenonEmden/ComponentWeights.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HenonLaneEmden.LineComponents.forwardExit_le_volume_component line 15
  2. lemma OAI.HenonLaneEmden.LineComponents.backwardExit_le_volume_component line 31
  3. lemma OAI.HenonLaneEmden.LineComponents.volume_component_all line 48

    Source documentation

    The rational exit construction gives the genuine Lebesgue length, including unbounded components, not merely the finite case.

    lemma volume_component_all {U : Set (X × ℝ)} (hU : IsOpen U) {p : X}
    (hp : (p,0) ∈ U) :
    volume (connectedComponentIn {s : ℝ | (p,s) ∈ U} 0) = componentLength U p := by
…

    Mentions: OAI.HenonLaneEmden.LineComponents.componentLength

  4. def OAI.HenonLaneEmden.LineComponents.shiftedLayer line 62

    Source documentation

    The family that observes a single real layer relative to a moving basepoint.

    def shiftedLayer (U : Set ℝ) : Set (ℝ × ℝ) := {z | z.1+z.2 ∈ U}
  5. lemma OAI.HenonLaneEmden.LineComponents.isOpen_shiftedLayer line 64
  6. lemma OAI.HenonLaneEmden.LineComponents.image_relative_component line 67
  7. lemma OAI.HenonLaneEmden.LineComponents.shifted_componentInf_eq line 81
  8. lemma OAI.HenonLaneEmden.LineComponents.shifted_componentLength_eq line 88
  9. lemma OAI.HenonLaneEmden.LineComponents.bounded_of_connected_volume_ne_top line 100

    Source documentation

    A connected real set of finite length is bounded; this rules out every unbounded line-component case without choosing fictitious infinite endpoints.

    lemma bounded_of_connected_volume_ne_top {I : Set ℝ} (hc : IsConnected I)
    (hv : volume I ≠ ⊤) : BddBelow I ∧ BddAbove I := by
…
  10. def OAI.HenonLaneEmden.LineComponents.setInf line 121
  11. def OAI.HenonLaneEmden.LineComponents.setWeight line 126

    Source documentation

    The component weight, including the zero continuation when the set is empty or the length condition fails.

    noncomputable def setWeight (h d : ℝ → ℝ) (δ : ℝ) (I : Set ℝ) : ℝ≥0∞ :=
…
  12. lemma OAI.HenonLaneEmden.LineComponents.setInf_le line 130
  13. lemma OAI.HenonLaneEmden.LineComponents.setWeight_le line 134
  14. lemma OAI.HenonLaneEmden.LineComponents.setWeight_ne_top line 141
  15. lemma OAI.HenonLaneEmden.LineComponents.setWeight_eq_zero_of_empty line 149
  16. lemma OAI.HenonLaneEmden.LineComponents.setWeight_pos_bounded line 152
  17. lemma OAI.HenonLaneEmden.LineComponents.componentWeight_eq_setWeight line 161
  18. lemma OAI.HenonLaneEmden.LineComponents.shifted_componentWeight_eq line 175
  19. lemma OAI.HenonLaneEmden.LineComponents.measurable_setWeight_component line 187
  20. def OAI.HenonLaneEmden.LineComponents.relativeLayer line 202
  21. lemma OAI.HenonLaneEmden.LineComponents.isOpen_relativeLayer line 205
  22. lemma OAI.HenonLaneEmden.LineComponents.relative_componentWeight_eq line 208
  23. lemma OAI.HenonLaneEmden.LineComponents.measurable_parametric_setWeight line 223