OAI/Analysis/HenonEmden/Energy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HenonLaneEmden.energyDensity line 10
2. lemma OAI.HenonLaneEmden.measurable_energyDensity line 13
3. lemma OAI.HenonLaneEmden.energyDensity_nonneg line 18
4. lemma OAI.HenonLaneEmden.energyDensity_dilation line 22
5. lemma OAI.HenonLaneEmden.lintegral_ball_comp_dilation line 33
6. lemma OAI.HenonLaneEmden.lintegral_energy_dilation line 53
7. lemma OAI.HenonLaneEmden.energy_exponents line 68
8. lemma OAI.HenonLaneEmden.energyDensity_eq_source_mul line 74
9. lemma OAI.HenonLaneEmden.IsSolution.energy_locallyIntegrable line 79
10. lemma OAI.HenonLaneEmden.IsSolution.energy_ball_pos line 88
11. lemma OAI.HenonLaneEmden.IsSolution.energy_ball_finite line 103
12. lemma OAI.HenonLaneEmden.IsSolution.scaled_energy_unbounded line 111

    Source documentation

    The scaling obstruction. With the strict hyperbola, any putative solution has arbitrarily large unit-ball energy among its dilates.

    lemma IsSolution.scaled_energy_unbounded {n : ℕ} (hn : 2 ≤ n) {p q A B : ℝ}
        {u v : Space n → ℝ} (h : IsSolution n p q A B u v) (hp : 0 < p) (hq : 0 < q)
        (hsub : Subcritical n p q A B) (C : ℝ) :
        ∃ R : ℝ, 1 ≤ R ∧ ENNReal.ofReal C <
          ∫⁻ x in ball (0:Space n) 1,
            ENNReal.ofReal (energyDensity (dilation u (alpha p q A B) R) q B x) := by
    …

    Mentions: OAI.HenonLaneEmden.Space, OAI.HenonLaneEmden.IsSolution, OAI.HenonLaneEmden.Subcritical, OAI.HenonLaneEmden.energyDensity, OAI.HenonLaneEmden.dilation, OAI.HenonLaneEmden.alpha