DirichletContractions.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Normal contractions in the genuine zero-boundary Sobolev space

theorem OAI.RegularPointCoordinates.SobolevSpace.norm_compContraction_le line 18
Source documentation
A scalar normal contraction decreases the full Sobolev norm.
```
theorem SobolevSpace.norm_compContraction_le {φ : ℝ → ℝ}
    (hφ : LipschitzWith 1 φ) (hφ0 : φ 0 = 0) (f : SobolevSpace μ hQ) :
    ‖SobolevSpace.compContraction μ hQ hφ hφ0 f‖ ≤ ‖f‖ := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.compContraction
theorem OAI.RegularPointCoordinates.SobolevSpace.compContraction_mem_dirichletCore line 32
Source documentation
Composition preserves the compactly supported Lipschitz core.
```
theorem SobolevSpace.compContraction_mem_dirichletCore {φ : ℝ → ℝ}
    (hφ : LipschitzWith 1 φ) (hφ0 : φ 0 = 0) (Ω : Set X)
    (f : SobolevSpace μ hQ) (hf : f ∈ SobolevSpace.dirichletCore μ hQ Ω) :
    SobolevSpace.compContraction μ hQ hφ hφ0 f ∈
      SobolevSpace.dirichletCore μ hQ Ω := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.dirichletCore, OAI.RegularPointCoordinates.SobolevSpace.compContraction

theorem OAI.RegularPointCoordinates.SobolevSpace.mem_dirichlet_of_bounded_L2_limit line 46

Source documentation

Bounded energy and strong L² convergence suffice to retain membership in the closed Dirichlet subspace.

theorem SobolevSpace.mem_dirichlet_of_bounded_L2_limit (Ω : Set X)
    {fs : ℕ → SobolevSpace μ hQ} {f : SobolevSpace μ hQ} {C : ℝ}
    (hmem : ∀ i, fs i ∈ SobolevSpace.dirichlet μ hQ Ω)
    (hbound : ∀ i, ‖fs i‖ ≤ C)
    (hlim : Tendsto (fun i => SobolevSpace.toLp μ hQ (fs i)) atTop
      (𝓝 (SobolevSpace.toLp μ hQ f))) :
    f ∈ SobolevSpace.dirichlet μ hQ Ω := by
…

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

theorem OAI.RegularPointCoordinates.SobolevSpace.compContraction_mem_dirichlet line 67
Source documentation
The closed zero-boundary space is stable under every scalar normal contraction. Strong continuity of composition in H¹ is not assumed.
```
theorem SobolevSpace.compContraction_mem_dirichlet {φ : ℝ → ℝ}
    (hφ : LipschitzWith 1 φ) (hφ0 : φ 0 = 0) (Ω : Set X)
    (f : SobolevSpace μ hQ) (hf : f ∈ SobolevSpace.dirichlet μ hQ Ω) :
    SobolevSpace.compContraction μ hQ hφ hφ0 f ∈
      SobolevSpace.dirichlet μ hQ Ω := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.compContraction