OAI/Analysis/HenonEmden/ShortComponents.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HenonLaneEmden.LineComponents.dist_le_component_volume line 11
2. lemma OAI.HenonLaneEmden.LineComponents.dist_le_of_volume_le line 20
3. lemma OAI.HenonLaneEmden.LineComponents.setInf_lower line 25
4. lemma OAI.HenonLaneEmden.LineComponents.short_setWeight_eq line 35

   Source documentation

   Every short component passes the component length test. The bound on d is kept intrinsic, so no choice of coordinates enters the statement.

   lemma short_setWeight_eq {I : Set ℝ} (hI : I.Nonempty)
       {h d : ℝ → ℝ} {δ d₀ l : ℝ} (hδ : 0 ≤ δ) (hδ' : δ ≤ 1/2)
       (hd₀ : 0 ≤ d₀) (_hl : 0 ≤ l) (hl' : l ≤ δ*d₀)
       (hv : volume I ≤ ENNReal.ofReal l) (hd : ∀ y ∈ I, d₀-l ≤ d y) :
       setWeight h d δ I = setInf h I := by
   …

   Mentions: OAI.HenonLaneEmden.LineComponents.setWeight, OAI.HenonLaneEmden.LineComponents.setInf

5. lemma OAI.HenonLaneEmden.LineComponents.setInf_oscillation line 52
6. lemma OAI.HenonLaneEmden.LineComponents.short_component_loss line 66