DyadicBochnerMass.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual scaled Bochner masses and their Gaussian envelope

def OAI.RegularPointCoordinates.dyadicBochnerMass line 19
Source documentation
The full positive Bochner measure on a fixed-root dyadic ball, with the dimensional scaling used by the heat decrement.
```
def dyadicBochnerMass (M : PositiveBilinearMeasure X E) (n : ℕ)
    (p : X) (R : ℝ) (i : ℕ) : E →L[ℝ] E :=
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure
theorem OAI.RegularPointCoordinates.dyadicBochnerMass_isPositive line 23
theorem OAI.RegularPointCoordinates.dyadicBochnerMass_inner line 29
theorem OAI.RegularPointCoordinates.bochner_total_mass_le line 39
Source documentation
The fixed finite source has a single operator-norm bound for its total mass in every direction. No absolute continuity is required.
```
theorem bochner_total_mass_le (M : PositiveBilinearMeasure X E) (v : E) :
    (M.measure v).real univ ≤ ‖M.massOperator univ‖ * ‖v‖ ^ 2 := by
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure
def OAI.RegularPointCoordinates.dyadicBochnerEnvelope line 49
Source documentation
The actual positive mass envelope used in the cumulative comparison.
```
def dyadicBochnerEnvelope (M : PositiveBilinearMeasure X E) (n : ℕ)
    (p : X) (R : ℝ) (i : ℕ) : E →L[ℝ] E :=
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure
theorem OAI.RegularPointCoordinates.dyadicBochnerEnvelope_isPositive line 54
theorem OAI.RegularPointCoordinates.dyadicBochnerEnvelope_inner line 64