MeanNorm.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.GammaFPP.rationalMean_lower line 11

Source documentation

Positive denominators transport a lattice coercivity bound to rationals.

lemma rationalMean_lower (m : Vertex → ℝ) (c : ℝ)
    (hm : ∀ x, c * (|(x.1 : ℝ)| + |(x.2 : ℝ)|) ≤ m x)
    (q : ℚ × ℚ) :
    c * (|(q.1 : ℝ)| + |(q.2 : ℝ)|) ≤ rationalMean m q := by
…

Mentions: OAI.GammaFPP.rationalMean

lemma OAI.GammaFPP.realMeanExtension_lower line 33

Source documentation

A closed inequality on the rational image holds on its real closure.

lemma realMeanExtension_lower {f : ℚ × ℚ → ℝ} (hf : UniformContinuous f)
    (c : ℝ) (hl : ∀ q, c * (|(q.1 : ℝ)| + |(q.2 : ℝ)|) ≤ f q)
    (v : ℝ × ℝ) : c * (|v.1| + |v.2|) ≤ realMeanExtension f v := by
…

Mentions: OAI.GammaFPP.realMeanExtension

lemma OAI.GammaFPP.gammaMeanPairSeminorm_lower line 48
def OAI.GammaFPP.gammaMeanNorm line 64
Source documentation
Literal Euclidean-plane pullback of the actual mean seminorm.
```
noncomputable def gammaMeanNorm
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (v : Plane) : ℝ := gammaMeanPairSeminorm h hs hr (v 0, v 1)
```
Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.gammaMeanPairSeminorm
lemma OAI.GammaFPP.gammaMeanNorm_lower line 68
theorem OAI.GammaFPP.gammaMeanNorm_laws line 74
Source documentation
The real extension of the Gamma directional mean constants is a norm.
```
theorem gammaMeanNorm_laws
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate) :
    TimeConstantNorm (gammaMeanNorm h hs hr) := by
…
```
Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.gammaMeanNorm