L2LevelMeasure.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.RegularPointCoordinates.lp_level_measure_le line 17
Source documentation
A lower bound on a finite-measure set gives the corresponding L2 level-set estimate, with the actual chosen representative.
```
theorem lp_level_measure_le (u : Lp ℝ 2 μ) {A : Set X} (hAt : μ A ≠ ∞)
    {t : ℝ} (ht : 0 ≤ t) (hbound : ∀ᵐ x ∂μ.restrict A, t ≤ |u x|) :
    t^2 * μ.real A ≤ ‖u‖^2 := by
…
```
theorem OAI.RegularPointCoordinates.dirichlet_integral_square_eq_norm_square line 34
Source documentation
Zero boundary values identify the full L2 norm with the integral on the Dirichlet domain.
```
theorem dirichlet_integral_square_eq_norm_square [MetricSpace X]
    (hQ : QuadraticCheegerEnergy μ) {Ω : Set X} (hΩ : MeasurableSet Ω)
    (w : SobolevSpace.dirichlet μ hQ Ω) :
    (∫ x in Ω, (SobolevSpace.toLp μ hQ w.val x)^2 ∂μ) =
      ‖SobolevSpace.toLp μ hQ w.val‖^2 := by
…
```
Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp