DirichletPoincare.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

RCD coercivity for the actual zero-boundary Sobolev space

A positive-measure exterior set gives the Poincare constant required by the Dirichlet solver. The estimate is deduced from the existing RCD transport proof of integral coercivity.

theorem OAI.RegularPointCoordinates.lp_integral_square_eq_norm_square line 23

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_dirichlet_poincare line 30

Source documentation

A bounded Dirichlet domain with positive-measure exterior has an explicit finite Poincare constant.

theorem NoncollapsedRCD.exists_dirichlet_poincare
    (K : ℝ) (n : ℕ) (hn : 2 ≤ n) (hX : NoncollapsedRCD K n X)
    (p : X) {R : ℝ} (hR : 0 ≤ R) (Ω B : Set X)
    (hΩ : MeasurableSet Ω) (hB : MeasurableSet B)
    (hΩ0 : hausdorff n X Ω ≠ 0) (hB0 : hausdorff n X B ≠ 0)
    (hsΩ : Ω ⊆ Metric.closedBall p R) (hsB : B ⊆ Metric.closedBall p R)
    (hBΩ : B ⊆ Ωᶜ) :
    ∃ P : ℝ, 0 ≤ P ∧
      ∀ f : SobolevSpace.dirichlet (hausdorff n X) hX.quadratic Ω,
        ‖SobolevSpace.toLp (hausdorff n X) hX.quadratic f.val‖ ^ 2 ≤
          P * energyForm (hausdorff n X) hX.quadratic f.val f.val := by
…

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

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_dirichlet_harmonic_replacement line 67

Source documentation

The harmonic replacement exists for the genuine RCD Dirichlet form; its coercivity is derived above, rather than supplied as an extra input.

theorem NoncollapsedRCD.exists_dirichlet_harmonic_replacement
    (K : ℝ) (n : ℕ) (hn : 2 ≤ n) (hX : NoncollapsedRCD K n X)
    (p : X) {R : ℝ} (hR : 0 ≤ R) (Ω B : Set X)
    (hΩ : MeasurableSet Ω) (hB : MeasurableSet B)
    (hΩ0 : hausdorff n X Ω ≠ 0) (hB0 : hausdorff n X B ≠ 0)
    (hsΩ : Ω ⊆ Metric.closedBall p R) (hsB : B ⊆ Metric.closedBall p R)
    (hBΩ : B ⊆ Ωᶜ) (u : SobolevSpace (hausdorff n X) hX.quadratic) :
    ∃ h : SobolevSpace (hausdorff n X) hX.quadratic,
      h - u ∈ SobolevSpace.dirichlet (hausdorff n X) hX.quadratic Ω ∧
      IsSobolevHarmonicOn (hausdorff n X) hX.quadratic Ω h := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.IsSobolevHarmonicOn

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_dirichlet_harmonic_column line 83

Source documentation

Componentwise replacement constructs the full harmonic coordinate column without assuming a harmonic solution as data.

theorem NoncollapsedRCD.exists_dirichlet_harmonic_column
    (K : ℝ) (n : ℕ) (hn : 2 ≤ n) (hX : NoncollapsedRCD K n X)
    (p : X) {R : ℝ} (hR : 0 ≤ R) (Ω B : Set X)
    (hΩ : MeasurableSet Ω) (hB : MeasurableSet B)
    (hΩ0 : hausdorff n X Ω ≠ 0) (hB0 : hausdorff n X B ≠ 0)
    (hsΩ : Ω ⊆ Metric.closedBall p R) (hsB : B ⊆ Metric.closedBall p R)
    (hBΩ : B ⊆ Ωᶜ) (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic) :
    ∃ h : Fin n → SobolevSpace (hausdorff n X) hX.quadratic,
      ∀ a, h a - u a ∈ SobolevSpace.dirichlet (hausdorff n X) hX.quadratic Ω ∧
        IsSobolevHarmonicOn (hausdorff n X) hX.quadratic Ω (h a) := by
…