OAI/Analysis/BernoulliCone/HarmonicReplacement.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.SobolevCalculus.energy_positivePart_le line 17
2. lemma OAI.Bernoulli.SobolevCalculus.compare_signed line 35

   Source documentation

   Full comparison with arbitrary signed Sobolev competitors follows from precisely the nonnegative-competitor convention of the paper.

   lemma compare_signed [IsFiniteMeasure (volume.restrict D)] (hD : IsOpen D)
       (hu : H1 D u G) (hn : ∀ᵐ x ∂volume.restrict D, 0 ≤ u x)
       (hmin : ∀ (v : Space d → ℝ) (V : Space d → Space d),
         H1 D v V → (∀ᵐ x ∂volume.restrict D, 0 ≤ v x) →
         H10 D (fun x => v x - u x) (fun x => V x - G x) →
         energy D u G ≤ energy D v V)
       (hv : H1 D v V) (hvu : H10 D (fun x => v x-u x) (fun x => V x-G x)) :
       energy D u G ≤ energy D v V := by
   …

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

3. lemma OAI.Bernoulli.SobolevCalculus.energy_affine_le line 47
4. lemma OAI.Bernoulli.SobolevCalculus.linear_coefficient_nonpositive line 80
5. lemma OAI.Bernoulli.SobolevCalculus.subharmonic_of_comparison line 96

   Source documentation

   Distributional subharmonicity follows without any continuity or pointwise positivity assumption on the unknown minimizer.

   lemma subharmonic_of_comparison [IsFiniteMeasure (volume.restrict D)] (hD : IsOpen D)
       (hu : H1 D u G) (hn : ∀ᵐ x ∂volume.restrict D, 0 ≤ u x)
       (hmin : ∀ (v : Space d → ℝ) (V : Space d → Space d),
         H1 D v V → (∀ᵐ x ∂volume.restrict D, 0 ≤ v x) →
         H10 D (fun x => v x - u x) (fun x => V x - G x) →
         energy D u G ≤ energy D v V)
       {φ : Space d → ℝ} (hφ : Test D φ)
       (hφn : ∀ᵐ x ∂volume.restrict D, 0 ≤ φ x) :
       (∫ x in D, inner ℝ (G x) (gradient φ x)) ≤ 0 := by
   …

   Mentions: OAI.Bernoulli.H1, OAI.Bernoulli.Space, OAI.Bernoulli.H10, OAI.Bernoulli.energy, OAI.Bernoulli.Test

6. lemma OAI.Bernoulli.LocalMinimizer.subharmonic line 125
7. lemma OAI.Bernoulli.LocalMinimizer.compare_signed line 139
8. lemma OAI.Bernoulli.SobolevCalculus.gradient_norm_eq line 163
9. lemma OAI.Bernoulli.SobolevCalculus.test_gradient_norm line 167
10. lemma OAI.Bernoulli.SobolevCalculus.test_poincare line 174
11. lemma OAI.Bernoulli.SobolevCalculus.tendsto_eLpNorm_of_strong line 216
12. lemma OAI.Bernoulli.SobolevCalculus.h10_poincare line 228

    Source documentation

    The Poincare inequality holds for arbitrary H1_0 competitors, not just smooth or pointwise regular functions.

    lemma h10_poincare (hd : 2 ≤ d) (hD : Bornology.IsBounded D) :
        ∃ C : ℝ≥0, ∀ (u : Space d → ℝ) (G : Space d → Space d), H10 D u G →
          eLpNorm u 2 (volume.restrict D) ≤ C * eLpNorm G 2 (volume.restrict D) := by
    …

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

13. lemma OAI.Bernoulli.Test.zero line 248
14. lemma OAI.Bernoulli.Test.add line 251
15. lemma OAI.Bernoulli.Test.gradient_add line 256
16. lemma OAI.Bernoulli.Test.sub line 265
17. lemma OAI.Bernoulli.Test.gradient_sub line 271
18. lemma OAI.Bernoulli.H10.const_smul line 280
19. lemma OAI.Bernoulli.H10.neg line 300
20. abbrev OAI.Bernoulli.HarmonicReplacement.VectorLp line 306
21. abbrev OAI.Bernoulli.HarmonicReplacement.ScalarLp line 307
22. def OAI.Bernoulli.HarmonicReplacement.testGradients line 310

    Source documentation

    Actual gradients of compactly supported smooth tests, in L2.

    def testGradients (D : Set (Space d)) : Submodule ℝ (VectorLp D) where
    …

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.HarmonicReplacement.VectorLp

23. def OAI.Bernoulli.HarmonicReplacement.zeroGradients line 331

    Source documentation

    Closed gradient space used for Dirichlet harmonic replacement.

    def zeroGradients (D : Set (Space d)) : Submodule ℝ (VectorLp D) :=
    …

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.HarmonicReplacement.VectorLp

24. lemma OAI.Bernoulli.HarmonicReplacement.h10_mem_zeroGradients line 334
25. lemma OAI.Bernoulli.HarmonicReplacement.test_poincare_norm line 344
26. lemma OAI.Bernoulli.HarmonicReplacement.zeroGradients_h10 line 353
27. theorem OAI.Bernoulli.HarmonicReplacement.exists_replacement line 390
28. lemma OAI.Bernoulli.HarmonicReplacement.orthogonal_energy_identity line 416
29. lemma OAI.Bernoulli.HarmonicReplacement.replacement_energy_estimate line 439

    Source documentation

    The Bernoulli term is retained in the harmonic-replacement estimate.

    lemma replacement_energy_estimate [IsFiniteMeasure (volume.restrict D)]
        {u h : Space d → ℝ} {G H : Space d → Space d}
        (hu : H1 D u G) (hh : H1 D h H)
        (ht : H10 D (h-u) (H-G))
        (ho : ∀ v V, H10 D v V → (∫ x in D, inner ℝ (H x) (V x)) = 0)
        (hmin : energy D u G ≤ energy D h H) :
        (∫ x in D, ‖(G-H) x‖^2) +
          (∫ x in D, if 0 < u x then (1 : ℝ) else 0) ≤ (volume D).toReal := by
    …

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

30. lemma OAI.Bernoulli.LocalMinimizer.harmonic_replacement line 469

    Source documentation

    Actual Bernoulli minimizers admit harmonic replacements with the full volume-term estimate, without a regularity assumption on the minimizer.

    lemma LocalMinimizer.harmonic_replacement (hd : 2 ≤ d)
        {u : Space d → ℝ} (hu : LocalMinimizer D u) :
        ∃ G : Space d → Space d, H1Loc D u G ∧
          ∀ (c : Space d) (r : ℝ), 0 < r → Metric.closedBall c r ⊆ D →
          ∃ (h : Space d → ℝ) (H : Space d → Space d),
            H1 (Metric.ball c r) h H ∧ H10 (Metric.ball c r) (h-u) (H-G) ∧
            (∀ v V, H10 (Metric.ball c r) v V →
              (∫ x in Metric.ball c r, inner ℝ (H x) (V x)) = 0) ∧
            (∫ x in Metric.ball c r, ‖(G-H) x‖^2) +
              (∫ x in Metric.ball c r, if 0 < u x then (1 : ℝ) else 0) ≤
                (volume (Metric.ball c r)).toReal := by
    …

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.LocalMinimizer, OAI.Bernoulli.H1Loc, OAI.Bernoulli.H1, OAI.Bernoulli.H10