Angular.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HenonLaneEmden.Angular.ray_mass_le line 19

Source documentation

Polar lower bound contributed by a set of directions whose full radial segment has source at least t. Surface measure here is not normalized.

lemma ray_mass_le {f : E → ℝ≥0∞} {S : Set (sphere (0:E) 1)}
    (hS : MeasurableSet S) {l : ℝ} (hl : 0 < l) (t : ℝ≥0∞)
    (h : ∀ e ∈ S, ∀ r ∈ Ioo 0 l, t ≤ f (r • e.1)) :
    t * μ.toSphere S * ENNReal.ofReal (l ^ Module.finrank ℝ E / Module.finrank ℝ E)
      ≤ ∫⁻ z, f z ∂μ := by
…

lemma OAI.HenonLaneEmden.Angular.long_component_mass_le line 50

Source documentation

The long-component alternative on a line uses either forward or backward rays. In particular it requires no independence of any cap weight and layer.

lemma long_component_mass_le {f : E → ℝ≥0∞}
    {U : Set (sphere (0:E) 1 × ℝ)} (hU : IsOpen U)
    {l : ℝ} (hl : 0 < l) (t : ℝ≥0∞)
    (h : ∀ e r, |r| ≤ l/2 → (e,r) ∈ U → t ≤ f (r • e.1)) :
    t * ENNReal.ofReal ((l/2)^Module.finrank ℝ E / Module.finrank ℝ E) *
      μ.toSphere {e | ENNReal.ofReal l < componentLength U e} ≤
      2 * ∫⁻ z, f z ∂μ := by
…

lemma OAI.HenonLaneEmden.Angular.long_component_local_mass_le line 93

Source documentation

Translation of the ray estimate to a local source; the only quantitative input is its mass on the fixed ball B₄.

lemma long_component_local_mass_le {f : E → ℝ} {x : E} (hx : ‖x‖ ≤ 2)
    {t l : ℝ} (hl : 0 < l) (hl1 : l ≤ 1)
    (hU : IsOpen {z : sphere (0:E) 1 × ℝ | t < f (x + z.2 • z.1.1)}) :
    ENNReal.ofReal t * ENNReal.ofReal ((l/2)^Module.finrank ℝ E / Module.finrank ℝ E) *
      μ.toSphere {e | ENNReal.ofReal l < componentLength
        {z : sphere (0:E) 1 × ℝ | t < f (x + z.2 • z.1.1)} e} ≤
      2 * ∫⁻ z in ball (0:E) 4, ENNReal.ofReal (f z) ∂μ := by
…

lemma OAI.HenonLaneEmden.isOpen_source_subgraph line 120
Source documentation
With value zero assigned at the origin, the positive source subgraph is open jointly in spatial location and positive level.
```
lemma isOpen_source_subgraph {n : ℕ} {u : Space n → ℝ}
    (hu : ContDiffOn ℝ 2 u ({0}ᶜ : Set (Space n))) (hup : ∀ x, 0 < u x) (q B : ℝ) :
    IsOpen {z : Space n × ℝ | 0 < z.2 ∧ z.2 < source u q B z.1} := by
…
```
Mentions: OAI.HenonLaneEmden.Space, OAI.HenonLaneEmden.source
lemma OAI.HenonLaneEmden.isOpen_source_lineLayer line 133