theorem
exp_ineq_ENN
{V : Type}
{X : Finset V}
[MeasurableSpace { x : V // x ∈ X }]
{ℙᵤ : MeasureTheory.Measure ({ x : V // x ∈ X } × { x : V // x ∈ X })}
[dm : DiscreteMeasurableSpace ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[MeasurableSingletonClass ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[MeasureTheory.IsProbabilityMeasure ℙᵤ]
{r : ℕ}
(rpos : 0 < r)
(Z : Fin r → { x : V // x ∈ X } × { x : V // x ∈ X } → ℝ)
(exPos :
0 ≤ ∫ (x : { x : V // x ∈ X } × { x : V // x ∈ X }), (fun (xx : { x : V // x ∈ X } × { x : V // x ∈ X }) => f fun (i : Fin r) => Z i xx) x ∂ℙᵤ)
:
theorem
lintegral_sum_bound
{r : ℕ}
{V : Type}
{X : Finset V}
[MeasurableSpace { x : V // x ∈ X }]
{ℙᵤ : MeasureTheory.Measure ({ x : V // x ∈ X } × { x : V // x ∈ X })}
[dm : DiscreteMeasurableSpace ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[MeasurableSingletonClass ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[Fintype V]
[nenr : Nonempty (Fin r)]
(σ : Fin r → { x : V // x ∈ X } → V → ℝ)
:
have β := oℝ (3 ^ (-4 * ↑r));
have C := 4 * ↑r * oℝ √↑r;
have τ := fun (x : { x : V // x ∈ X } × { x : V // x ∈ X }) (i : Fin r) => σ i x.1 ⬝ᵥ σ i x.2;
have Z := fun (i : Fin r) (x : { x : V // x ∈ X } × { x : V // x ∈ X }) => 3 * ↑r * τ x i;
have E := {xx : { x : V // x ∈ X } × { x : V // x ∈ X } | ∀ (i : Fin r), -3 * ↑r ≤ Z i xx};
have nenI := ⋯;
have M := fun (x : { x : V // x ∈ X } × { x : V // x ∈ X }) => (Finset.image (τ x) Finset.univ).max' ⋯;
have c := oℝ (↑r * √(3 * ↑r));
ℙᵤ E < β →
(∀ (y : ℝ),
-1 ≤ y →
ℙᵤ (E ∩ {x : { x : V // x ∈ X } × { x : V // x ∈ X } | y ≤ M x}) < oℝ (Real.exp (-C.toReal * √(y + 1))) * β * ↑r) →
∫⁻ (x : { x : V // x ∈ X } × { x : V // x ∈ X }) in E, oℝ (Real.exp (∑ i : Fin r, √(Z i x + 3 * ↑r))) ∂ℙᵤ ≤ β * (↑r * c + 1)
theorem
expPos
{r : ℕ}
{V : Type}
{X : Finset V}
[MeasurableSpace { x : V // x ∈ X }]
{ℙᵤ : MeasureTheory.Measure ({ x : V // x ∈ X } × { x : V // x ∈ X })}
[dm : DiscreteMeasurableSpace ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[MeasurableSingletonClass ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[MeasureTheory.IsProbabilityMeasure ℙᵤ]
[Fintype V]
[nenr : Nonempty (Fin r)]
(σ : Fin r → { x : V // x ∈ X } → V → ℝ)
:
have τ := fun (x : { x : V // x ∈ X } × { x : V // x ∈ X }) (i : Fin r) => σ i x.1 ⬝ᵥ σ i x.2;
have Z := fun (i : Fin r) (x : { x : V // x ∈ X } × { x : V // x ∈ X }) => 3 * ↑r * τ x i;
0 ≤ ∫ (x : { x : V // x ∈ X } × { x : V // x ∈ X }), (fun (xx : { x : V // x ∈ X } × { x : V // x ∈ X }) => f fun (i : Fin r) => Z i xx) x ∂ℙᵤ
theorem
geometric
{r : ℕ}
{V : Type}
{X : Finset V}
[MeasurableSpace { x : V // x ∈ X }]
{ℙᵤ : MeasureTheory.Measure ({ x : V // x ∈ X } × { x : V // x ∈ X })}
[dm : DiscreteMeasurableSpace ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[MeasurableSingletonClass ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[MeasureTheory.IsProbabilityMeasure ℙᵤ]
[Fintype V]
[nenr : Nonempty (Fin r)]
(σ : Fin r → { x : V // x ∈ X } → V → ℝ)
:
have β := 3 ^ (-4 * ↑r);
have C := 4 * ↑r * √↑r;
have τ := fun (x : { x : V // x ∈ X } × { x : V // x ∈ X }) (i : Fin r) => σ i x.1 ⬝ᵥ σ i x.2;
∃ (Λ : ℝ),
-1 ≤ Λ ∧ ∃ (i : Fin r),
oℝ (β * Real.exp (-C * √(Λ + 1))) ≤ ℙᵤ {x : { x : V // x ∈ X } × { x : V // x ∈ X } | Λ ≤ τ x i ∧ ∀ (j : Fin r), j ≠ i → -1 ≤ τ x j}