OAI/Analysis/BernoulliCone/GroundState.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.GroundState.compact_extension_near_test line 16
2. lemma OAI.Bernoulli.GroundState.compact_green line 33
3. lemma OAI.Bernoulli.GroundState.local_green line 44
4. lemma OAI.Bernoulli.GroundState.local_green_integrable line 65
5. lemma OAI.Bernoulli.GroundState.square_ratio_test line 97
6. lemma OAI.Bernoulli.GroundState.picone_identity line 123
7. theorem OAI.Bernoulli.GroundState.picone_test line 142

   Source documentation

   Ground-state square completion for arbitrary compact smooth tests in a positive superharmonic domain. It is proved by the weak integration-by-parts identity, not inserted as an assumption about the explicit barrier.

   theorem picone_test (hD : IsOpen D) {Y φ : Space d → ℝ}
       (hY : ContDiffOn ℝ ∞ Y D) (hYp : ∀x∈D, 0<Y x)
       (hLap : ∀x∈D, Δ Y x≤0) (hφ : Test D φ) :
       (∫x, ‖gradient φ x-(φ x/Y x) • gradient Y x‖^2) ≤
         (∫x, ‖gradient φ x‖^2) := by
   …

   Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.Test

8. lemma OAI.Bernoulli.GroundState.drift_test_memLp line 163
9. lemma OAI.Bernoulli.GroundState.integral_norm_sq_eq line 191
10. lemma OAI.Bernoulli.GroundState.picone_test_eLpNorm line 199
11. theorem OAI.Bernoulli.GroundState.picone_h10_eLpNorm line 228

    Source documentation

    The full H¹₀ ground-state inequality. Fatou's lemma handles the singular coefficient at the boundary or cone vertex; no bounded-drift or Hardy hypothesis is imposed.

    theorem picone_h10_eLpNorm (hD : IsOpen D) {Y w : Space d → ℝ} {G : Space d → Space d}
        (hY : ContDiffOn ℝ ∞ Y D) (hYp : ∀x∈D, 0<Y x)
        (hLap : ∀x∈D, Δ Y x≤0) (hw : H10 D w G) :
        MemLp (fun x=>G x-(w x/Y x) • gradient Y x) 2 (volume.restrict D) ∧
        eLpNorm (fun x=>G x-(w x/Y x) • gradient Y x) 2 (volume.restrict D) ≤
          eLpNorm G 2 (volume.restrict D) := by
    …

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.H10

12. theorem OAI.Bernoulli.GroundState.picone_h10 line 270
13. lemma OAI.Bernoulli.GroundState.orthogonal_h10_of_tests line 280
14. theorem OAI.Bernoulli.GroundState.harmonic_h10 line 307