ConvexBounds.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.convex_derivative_fluctuation line 14

Source documentation

The deterministic three-point estimate used in pert:convex-bound. It requires convexity only on the original open parameter domain, not globally.

theorem convex_derivative_fluctuation {S : Set ℝ} {f g f' g' : ℝ → ℝ}
    (hf : ConvexOn ℝ S f) (hg : ConvexOn ℝ S g)
    {u ρ : ℝ} (hρ : 0 < ρ) (hm : u-ρ ∈ S) (hu : u ∈ S) (hp : u+ρ ∈ S)
    (hfu : HasDerivAt f (f' u) u)
    (hgm : HasDerivAt g (g' (u-ρ)) (u-ρ))
    (hgu : HasDerivAt g (g' u) u)
    (hgp : HasDerivAt g (g' (u+ρ)) (u+ρ)) :
    |f' u - g' u| ≤
      (|f (u-ρ) - g (u-ρ)| + 2*|f u-g u| + |f (u+ρ)-g (u+ρ)|) / ρ +
        g' (u+ρ) - g' (u-ρ) := by
…

theorem OAI.DilutedSpinGlass.integral_abs_le_sqrt_sq line 63
theorem OAI.DilutedSpinGlass.integral_deviation_le_sqrt_variance line 71

theorem OAI.DilutedSpinGlass.convexOn_integral line 82

Source documentation

Taking a root expectation preserves convexity on the original parameter domain. This does not extend the perturbation outside its factor-positive interval.

theorem convexOn_integral {S : Set ℝ} {F : Ω → ℝ → ℝ}
    (hS : Convex ℝ S) (hF : ∀ x, ConvexOn ℝ S (F x))
    (hi : ∀ u ∈ S, Integrable (fun x => F x u) μ) :
    ConvexOn ℝ S (fun u => ∫ x, F x u ∂μ) := by
…

theorem OAI.DilutedSpinGlass.convex_derivative_mean_bound line 98

Source documentation

The probabilistic three-point convexity estimate, with its genuine standard-deviation (rather than variance) scale.

theorem convex_derivative_mean_bound {S : Set ℝ} {F F' : Ω → ℝ → ℝ}
    {g g' : ℝ → ℝ} (hf : ∀ x, ConvexOn ℝ S (F x)) (hg : ConvexOn ℝ S g)
    {u ρ V : ℝ} (hρ : 0 < ρ)
    (hm : u-ρ ∈ S) (hu : u ∈ S) (hp : u+ρ ∈ S)
    (hfu : ∀ x, HasDerivAt (F x) (F' x u) u)
    (hgm : HasDerivAt g (g' (u-ρ)) (u-ρ))
    (hgu : HasDerivAt g (g' u) u) (hgp : HasDerivAt g (g' (u+ρ)) (u+ρ))
    (hD : Integrable (fun x => F' x u) μ)
    (hi : ∀ w ∈ S, MemLp (fun x => F x w) 2 μ)
    (he : ∀ w ∈ S, g w = ∫ x, F x w ∂μ)
    (hv : ∀ w ∈ S, variance (fun x => F x w) μ ≤ V) :
    (∫ x, |F' x u-g' u| ∂μ) ≤ 4*Real.sqrt V/ρ+g' (u+ρ)-g' (u-ρ) := by
…

theorem OAI.DilutedSpinGlass.integral_monotone_shift line 148
Source documentation
The boundary-layer estimate used in pert:convex-bound. It holds on the specified finite domain only, including when the two boundary layers overlap.
```
theorem integral_monotone_shift {k : ℝ → ℝ} {a b ρ : ℝ}
    (hab : a ≤ b) (hρ : 0 ≤ ρ) (hk : MonotoneOn k (Icc (a-ρ) (b+ρ))) :
    (∫ u in a..b, k (u+ρ)-k (u-ρ)) ≤ 2*ρ*(k (b+ρ)-k (a-ρ)) := by
…
```
theorem OAI.DilutedSpinGlass.integral_convex_derivative_bound line 195
theorem OAI.DilutedSpinGlass.hasDerivAt_rootMean line 234
theorem OAI.DilutedSpinGlass.rootMean_abs_le line 248

theorem OAI.DilutedSpinGlass.root_derivative_integral_bound line 258

Source documentation

Root fluctuation estimate after averaging the actual convex score; all differentiations of expectations are justified by the integrable random count bound.

theorem root_derivative_integral_bound {F G : X → ℝ → ℝ} {S : Set ℝ}
    (hS : IsOpen S) (hSc : Convex ℝ S)
    (hFm : ∀ u, Measurable (fun x => F x u))
    (hGm : Measurable (fun z : X × ℝ => G z.1 z.2))
    (hfc : ∀ x, ConvexOn ℝ S (F x))
    (hLp : ∀ u ∈ S, MemLp (fun x => F x u) 2 μ)
    {B : X → ℝ} (hB : Integrable B μ) (hb : ∀ x u, u ∈ S → |G x u| ≤ B x)
    (hd : ∀ x u, u ∈ S → HasDerivAt (F x) (G x u) u)
    {a b ρ V : ℝ} (hab : a < b) (hρ : 0 < ρ)
    (hJ : Icc (a-ρ) (b+ρ) ⊆ S)
    (hv : ∀ u ∈ Icc (a-ρ) (b+ρ), variance (fun x => F x u) μ ≤ V) :
    (∫ u in a..b, (∫ x, |G x u-∫ y, G y u ∂μ| ∂μ))/(b-a) ≤
…