ShiftBound.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

§02 growth estimates for negative and positive bias layers.

theorem OAI.GeneralMahler.ProjField.uniform_X_neg line 14
theorem OAI.GeneralMahler.ProjField.norm_IP_integrable line 38

theorem OAI.GeneralMahler.ProjField.negative_mean line 48

Source comment

split the mixed moment at 4(1+s), exterior small even compared to a (-s)

theorem negative_mean (hk : 1 ≤ K) :
    ∃ C ≥ (0:ℝ), ∀ q : ProjField m, q.Bound K → ∀ s ≥ (0:ℝ),
      q.avH (-s) ≤ C*(1+s)*a (-s) ∧ q.Bt (-s) ≤ C*(1+s) := by
…

Mentions: OAI.GeneralMahler.ProjField

theorem OAI.GeneralMahler.ProjField.positive_mean line 112
lemma OAI.GeneralMahler.ProjField.layers_growth line 121
Source comment
both bias and samples pointwise at most linear growth
```
lemma layers_growth (hk : 1 ≤ K) :
    ∃ C ≥ (0:ℝ), ∀ q : ProjField m, q.Bound K → ∀ s,
      ‖q.shift s‖ ≤ C*(1+|s|) := by
…
```
Mentions: OAI.GeneralMahler.ProjField