HarmonicEnergyBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Enlarging the bound of a fixed harmonic energy representative

def OAI.RegularPointCoordinates.LocalHarmonicEnergy.enlargeBound line 18

Source documentation

The energy function and its full measure equation are unchanged.

def LocalHarmonicEnergy.enlargeBound {U : E →L[ℝ] SobolevSpace μ hQ}
    {M : PositiveBilinearMeasure X E} {κ : ℝ} {p : X} {r : ℝ} {L H : ℝ≥0} {v : E}
    (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (hLH : (L : ℝ) ^ 2 ≤ (H : ℝ) ^ 2) : LocalHarmonicEnergy μ hQ U M κ p r H v where
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy