LevelTruncation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Two-level truncations in the Dirichlet space

These bounded tests give the superlevel iteration for the torsion function. Locality at both clipping levels proves the exact energy identity.

def OAI.RegularPointCoordinates.levelClip line 22
theorem OAI.RegularPointCoordinates.levelClip_lipschitz line 24
theorem OAI.RegularPointCoordinates.levelClip_zero line 33
def OAI.RegularPointCoordinates.levelTruncation line 37
theorem OAI.RegularPointCoordinates.levelTruncation_coe line 41
theorem OAI.RegularPointCoordinates.levelTruncation_mem_dirichlet line 47
theorem OAI.RegularPointCoordinates.levelTruncation_energy line 56
Source documentation
The bounded two-level test loses no energy in pairing with its source.
```
theorem levelTruncation_energy (u : SobolevSpace μ hQ) {k l : ℝ}
    (hk : 0 ≤ k) (hkl : k ≤ l) :
    energyForm μ hQ (levelTruncation μ hQ u hk hkl) (levelTruncation μ hQ u hk hkl) =
      energyForm μ hQ u (levelTruncation μ hQ u hk hkl) := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.levelTruncation

theorem OAI.RegularPointCoordinates.torsion_level_energy line 94

Source documentation

A unit-source torsion solution satisfies the exact truncated energy identity required for its superlevel iteration.

theorem torsion_level_energy (Ω : Set X) (u : SobolevSpace.dirichlet μ hQ Ω)
    (hsolve : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      energyForm μ hQ u.val φ.val = ∫ x in Ω, SobolevSpace.toLp μ hQ φ.val x ∂μ)
    {k l : ℝ} (hk : 0 ≤ k) (hkl : k ≤ l) :
    energyForm μ hQ (levelTruncation μ hQ u.val hk hkl) (levelTruncation μ hQ u.val hk hkl) =
      ∫ x in Ω, levelClip k l (SobolevSpace.toLp μ hQ u.val x) ∂μ := by
…

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