TopWeightIntegral.lean`

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Integrability and exact area scaling for the actual decaying top weights.

def OAI.LipschitzHilbert.planeDivide line 17
theorem OAI.LipschitzHilbert.planeDivide_apply line 21
theorem OAI.LipschitzHilbert.map_planeDivide line 25
theorem OAI.LipschitzHilbert.integrable_planeDivide line 36
theorem OAI.LipschitzHilbert.integral_planeDivide line 43
def OAI.LipschitzHilbert.topProfile line 49
theorem OAI.LipschitzHilbert.topProfile_nonnegative line 51
theorem OAI.LipschitzHilbert.topProfile_continuous line 54
theorem OAI.LipschitzHilbert.topProfile_integrable line 63
Source documentation
The fixed normalized profile is integrable once its decay exponent exceeds its two-dimensional domain.
```
theorem topProfile_integrable {D : ℝ} (hD : 2 < D) :
    Integrable (topProfile D) (volume.prod volume) := by
…
```
Mentions: OAI.LipschitzHilbert.topProfile
def OAI.LipschitzHilbert.SlopeBox.normalizedCoordinates line 81
Source documentation
Normalized top coordinates, using first a translation, then the slope shear, then the two independent dilations.
```
def normalizedCoordinates (T : SlopeBox) (K : ℝ) (hK : 0 < K) (z : ℝ × ℝ) : ℝ × ℝ :=
…
```
Mentions: OAI.LipschitzHilbert.SlopeBox
theorem OAI.LipschitzHilbert.SlopeBox.normalizedCoordinates_eq line 86
theorem OAI.LipschitzHilbert.SlopeBox.weight_eq_topProfile line 91
theorem OAI.LipschitzHilbert.SlopeBox.weight_integrable line 97
Source documentation
The actual top weight is integrable, uniformly over positions and slopes.
```
theorem weight_integrable (T : SlopeBox) {K D : ℝ} (hK : 0 < K) (hD : 2 < D) :
    Integrable (T.weight K D) (volume.prod volume) := by
…
```
Mentions: OAI.LipschitzHilbert.SlopeBox
theorem OAI.LipschitzHilbert.SlopeBox.integral_weight line 115
Source documentation
Exact area scaling: all dependence on the box and the dilation is K² * length * width, while the remaining integral is a fixed constant.
```
theorem integral_weight (T : SlopeBox) {K : ℝ} (hK : 0 < K) (D : ℝ) :
    (∫ z, T.weight K D z ∂volume.prod volume) =
      (2 ^ D * ∫ z, topProfile D z ∂volume.prod volume) *
        K ^ 2 * T.length * T.width := by
…
```
Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.topProfile