Bias.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Unique mean-bias choice (§02, biased projection lemma). We solve for arbitrary interior means w, later inserting the bias curve.

def OAI.GeneralMahler.meanEnergy line 13
lemma OAI.GeneralMahler.energy_integrable line 15
theorem OAI.GeneralMahler.meanEnergy_derivative line 22
def OAI.GeneralMahler.dualEnergy line 56
theorem OAI.GeneralMahler.dualEnergy_derivative line 58
lemma OAI.GeneralMahler.meanEnergy_lower line 63
theorem OAI.GeneralMahler.dualEnergy_lower line 76
Source comment
explicit bound also useful for uniform estimates
```
theorem dualEnergy_lower (w a : Rn m)
    {r : ℝ} (hr : 0 < r) (hu : closedBall w r ⊆ C) :
    r*‖a‖-(‖w‖+r)^2/2 ≤ dualEnergy C B w a := by
…
```
Mentions: OAI.GeneralMahler.Rn, OAI.GeneralMahler.dualEnergy
theorem OAI.GeneralMahler.bias_exists line 100
lemma OAI.GeneralMahler.pd_equiv line 118
theorem OAI.GeneralMahler.mean_injective line 131
def OAI.GeneralMahler.bias line 157
Source documentation
Unique bias at an interior mean; arbitrary value outside interior.
```
def bias (w : Rn m) : Rn m :=
…
```
Mentions: OAI.GeneralMahler.Rn
theorem OAI.GeneralMahler.bias_mean line 161
theorem OAI.GeneralMahler.bias_C_one line 166