SobolevLevelChain.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Exact gradient localization for bounded level truncations

The level-set locality of the Cheeger energy gives the chain rule for piecewise affine truncations without differentiability at their corners. These are the bounded tests for the local harmonic mean-value argument.

theorem OAI.RegularPointCoordinates.localGamma_eq_on_diff_level line 22
Source documentation
Equality up to a constant on a measurable level set identifies gradients.
```
theorem localGamma_eq_on_diff_level (f g h : SobolevSpace μ hQ) (c : ℝ) :
    ∀ᵐ x ∂μ, SobolevSpace.toLp μ hQ f x-SobolevSpace.toLp μ hQ g x = c →
      localGamma μ hQ f h x = localGamma μ hQ g h x := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma
def OAI.RegularPointCoordinates.upperLevelClip line 35
Source documentation
The scalar truncation on the interval from k to k+m.
```
def upperLevelClip (k m s : ℝ) : ℝ := min (max (s-k) 0) m
```
theorem OAI.RegularPointCoordinates.upperLevelClip_lipschitz line 37
theorem OAI.RegularPointCoordinates.upperLevelClip_zero line 45
def OAI.RegularPointCoordinates.SobolevSpace.upperLevelTruncation line 50
theorem OAI.RegularPointCoordinates.SobolevSpace.upperLevelTruncation_coe line 56

theorem OAI.RegularPointCoordinates.localGamma_upperLevelTruncation line 63

Source documentation

The localized bilinear chain rule for the bounded upper-level truncation.

theorem localGamma_upperLevelTruncation (f g : SobolevSpace μ hQ) {k m : ℝ}
    (hk : 0 ≤ k) (hm : 0 ≤ m) :
    localGamma μ hQ (f.upperLevelTruncation μ hQ hk hm) g =ᵐ[μ] fun x =>
      if k < SobolevSpace.toLp μ hQ f x ∧ SobolevSpace.toLp μ hQ f x < k+m
      then localGamma μ hQ f g x else 0 := by
…

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

theorem OAI.RegularPointCoordinates.localGamma_upperLevelTruncation_self line 95
Source documentation
The truncated square-gradient is the original square-gradient restricted to the open level strip, including the correct zero values at both corners.
```
theorem localGamma_upperLevelTruncation_self (f : SobolevSpace μ hQ) {k m : ℝ}
    (hk : 0 ≤ k) (hm : 0 ≤ m) :
    let v := f.upperLevelTruncation μ hQ hk hm
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
def OAI.RegularPointCoordinates.upperLevelPart line 112
Source documentation
The upper positive part is a contraction fixing zero for nonnegative levels.
```
def upperLevelPart (k s : ℝ) : ℝ := max (s-k) 0
```
theorem OAI.RegularPointCoordinates.upperLevelPart_lipschitz line 114
theorem OAI.RegularPointCoordinates.upperLevelPart_zero line 121
def OAI.RegularPointCoordinates.SobolevSpace.upperPositivePart line 124
theorem OAI.RegularPointCoordinates.SobolevSpace.upperPositivePart_coe line 130
theorem OAI.RegularPointCoordinates.localGamma_upperPositivePart line 138
Source documentation
The positive-part gradient agrees with the original gradient above the level and vanishes on and below it.
```
theorem localGamma_upperPositivePart (f g : SobolevSpace μ hQ) {k : ℝ}
    (hk : 0 ≤ k) :
    localGamma μ hQ (f.upperPositivePart μ hQ hk) g =ᵐ[μ] fun x =>
      if k < SobolevSpace.toLp μ hQ f x then localGamma μ hQ f g x else 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.toLp
theorem OAI.RegularPointCoordinates.localGamma_upperPositivePart_self line 159
Source documentation
The same localized chain rule holds for the square-gradient.
```
theorem localGamma_upperPositivePart_self (f : SobolevSpace μ hQ) {k : ℝ}
    (hk : 0 ≤ k) :
    let v := f.upperPositivePart μ hQ hk
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace