DirichletPoisson.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Dirichlet solutions from the canonical Cheeger energy

The only quantitative premise is the Poincare estimate on the actual zero-boundary Sobolev space. Lax--Milgram constructs the solution, including the harmonic replacement of a given Sobolev function.

def OAI.RegularPointCoordinates.sobolevEnergyForm line 24
theorem OAI.RegularPointCoordinates.sobolevEnergyForm_apply line 28
def OAI.RegularPointCoordinates.dirichletEnergyForm line 31
theorem OAI.RegularPointCoordinates.dirichletEnergyForm_apply line 38
theorem OAI.RegularPointCoordinates.dirichletEnergyForm_isCoercive line 42

theorem OAI.RegularPointCoordinates.existsUnique_dirichlet_solution line 58

Source documentation

Existence and uniqueness for every continuous functional on the zero-boundary Sobolev space. No solution is assumed.

theorem existsUnique_dirichlet_solution (Ω : Set X) {P : ℝ} (hP : 0 ≤ P)
    (hbound : ∀ f : SobolevSpace.dirichlet μ hQ Ω,
      ‖SobolevSpace.toLp μ hQ f.val‖ ^ 2 ≤ P * energyForm μ hQ f.val f.val)
    (F : SobolevSpace.dirichlet μ hQ Ω →L[ℝ] ℝ) :
    ∃! f : SobolevSpace.dirichlet μ hQ Ω,
      ∀ φ : SobolevSpace.dirichlet μ hQ Ω, energyForm μ hQ f.val φ.val = F φ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm

theorem OAI.RegularPointCoordinates.exists_harmonic_replacement line 81
Source documentation
The harmonic representative in a given affine Dirichlet class is constructed from its boundary datum and the Poincare estimate.
```
theorem exists_harmonic_replacement (Ω : Set X) {P : ℝ} (hP : 0 ≤ P)
    (hbound : ∀ f : SobolevSpace.dirichlet μ hQ Ω,
      ‖SobolevSpace.toLp μ hQ f.val‖ ^ 2 ≤ P * energyForm μ hQ f.val f.val)
    (u : SobolevSpace μ hQ) :
    ∃ h : SobolevSpace μ hQ, h - u ∈ SobolevSpace.dirichlet μ hQ Ω ∧
      IsSobolevHarmonicOn μ hQ Ω h := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsSobolevHarmonicOn
theorem OAI.RegularPointCoordinates.harmonic_replacement_energy_le line 99
Source documentation
The harmonic representative does not increase Dirichlet energy.
```
theorem harmonic_replacement_energy_le (Ω : Set X) (u h : SobolevSpace μ hQ)
    (hboundary : h - u ∈ SobolevSpace.dirichlet μ hQ Ω)
    (hharm : IsSobolevHarmonicOn μ hQ Ω h) :
    energyForm μ hQ h h ≤ energyForm μ hQ u u := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.energyForm