theorem
exp_indicator
{X : Type u_1}
(m : X × X → ℝ)
(E : Set (X × X))
(mp : ∀ (x : X × X), m x < -1 → x ∉ E)
(x : X × X)
(c : ENNReal)
(cpos : 0 < c)
(cnt : c ≠ ⊤)
:
let ecsq := fun (y : ℝ) => Real.exp (c.toReal * √(y + 1));
let ecsq' := fun (x : ℝ) => Real.exp (c.toReal * √(x + 1)) * (c.toReal * (1 / (2 * √(x + 1))));
ENNReal.ofReal (ecsq (m x)) * E.indicator 1 x = (∫⁻ (a : ℝ) in Set.Ioi (-1), ENNReal.ofReal (ecsq' a) * (E ∩ {x : X × X | a ≤ m x}).indicator (fun (x : X × X) => 1) x) + E.indicator (fun (x : X × X) => 1) x
theorem
exp_ineq
{r : ℕ}
(rpos : 0 < r)
{V : Type}
[Fintype V]
{X : Finset V}
[Nonempty { x : V // x ∈ X }]
[MeasurableSpace { x : V // x ∈ X }]
[MeasurableSingletonClass ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[dm : DiscreteMeasurableSpace ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[DecidableEq { x : V // x ∈ X }]
{ℙᵤ : MeasureTheory.Measure ({ x : V // x ∈ X } × { x : V // x ∈ X })}
[MeasureTheory.IsProbabilityMeasure ℙᵤ]
(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 ∂ℙᵤ)
:
let E := {xx : { x : V // x ∈ X } × { x : V // x ∈ X } | ∀ (i : Fin r), -3 * ↑r ≤ Z i xx};
let exp := fun (xx : { x : V // x ∈ X } × { x : V // x ∈ X }) =>
3 ^ r * ↑r * Real.exp (∑ i : Fin r, √(Z i xx + 3 * ↑r));
let 𝔼exp := ∫ (x : { x : V // x ∈ X } × { x : V // x ∈ X }) in E, exp x ∂ℙᵤ;
1 - (ℙᵤ E).toReal ≤ 𝔼exp
theorem
exp_ineq_ENN
{r : ℕ}
(rpos : 0 < r)
{V : Type}
[Fintype V]
{X : Finset V}
[Nonempty { x : V // x ∈ X }]
[MeasurableSpace { x : V // x ∈ X }]
[MeasurableSingletonClass ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[dm : DiscreteMeasurableSpace ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[DecidableEq { x : V // x ∈ X }]
{ℙᵤ : MeasureTheory.Measure ({ x : V // x ∈ X } × { x : V // x ∈ X })}
[MeasureTheory.IsProbabilityMeasure ℙᵤ]
(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 ∂ℙᵤ)
:
let E := {xx : { x : V // x ∈ X } × { x : V // x ∈ X } | ∀ (i : Fin r), -3 * ↑r ≤ Z i xx};
let exp := fun (x : { x : V // x ∈ X } × { x : V // x ∈ X }) => 3 ^ r * ↑r * Real.exp (∑ i : Fin r, √(Z i x + 3 * ↑r));
1 - ℙᵤ E ≤ ∫⁻ (x : { x : V // x ∈ X } × { x : V // x ∈ X }) in E, ENNReal.ofReal (exp x) ∂ℙᵤ
theorem
integral_bound
{r : ℕ}
{V : Type}
[Fintype V]
{X : Finset V}
[MeasurableSpace { x : V // x ∈ X }]
[dm : DiscreteMeasurableSpace ({ x : V // x ∈ X } × { x : V // x ∈ X })]
{ℙᵤ : MeasureTheory.Measure ({ x : V // x ∈ X } × { x : V // x ∈ X })}
[MeasureTheory.IsProbabilityMeasure ℙᵤ]
{M : { x : V // x ∈ X } × { x : V // x ∈ X } → ℝ}
{E : Set ({ x : V // x ∈ X } × { x : V // x ∈ X })}
(mp : ∀ (x : { x : V // x ∈ X } × { x : V // x ∈ X }), M x < -1 → x ∉ E)
(measInter :
Measurable fun (a : ({ x : V // x ∈ X } × { x : V // x ∈ X }) × ℝ) =>
(E ∩ {x : { x : V // x ∈ X } × { x : V // x ∈ X } | a.2 ≤ M x}).indicator
(fun (x : { x : V // x ∈ X } × { x : V // x ∈ X }) => 1) a.1)
{c C : ENNReal}
(cpos : 0 < c)
(cnt : c ≠ ⊤)
(cleC : c.toReal ≤ C.toReal - 1)
:
let β := ENNReal.ofReal (3 ^ (-4 * ↑r));
let ecsq := fun (y : ℝ) => Real.exp (c.toReal * √(y + 1));
ℙᵤ E < β →
(∀ (y : ℝ),
-1 ≤ y →
ℙᵤ (E ∩ {x : { x : V // x ∈ X } × { x : V // x ∈ X } | y ≤ M x}) < ENNReal.ofReal (Real.exp (-C.toReal * √(y + 1))) * β * ↑r) →
∫⁻ (x : { x : V // x ∈ X } × { x : V // x ∈ X }) in E, ENNReal.ofReal (ecsq (M x)) ∂ℙᵤ ≤ β * (↑r * c + 1)
theorem
lintegral_sum_bound
{r : ℕ}
{V : Type}
[Fintype V]
[nenr : Nonempty (Fin r)]
{X : Finset V}
[Nonempty { x : V // x ∈ X }]
[MeasurableSpace { x : V // x ∈ X }]
[MeasurableSingletonClass ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[dm : DiscreteMeasurableSpace ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[DecidableEq { x : V // x ∈ X }]
{ℙᵤ : MeasureTheory.Measure ({ x : V // x ∈ X } × { x : V // x ∈ X })}
[MeasureTheory.IsProbabilityMeasure ℙᵤ]
{σ : Fin r → { x : V // x ∈ X } → V → ℝ}
:
let β := ENNReal.ofReal (3 ^ (-4 * ↑r));
let C := 4 * ↑r * ENNReal.ofReal √↑r;
let τ := fun (x : { x : V // x ∈ X } × { x : V // x ∈ X }) (i : Fin r) => σ i x.1 ⬝ᵥ σ i x.2;
let Z := fun (i : Fin r) (x : { x : V // x ∈ X } × { x : V // x ∈ X }) => 3 * ↑r * τ x i;
let E := {xx : { x : V // x ∈ X } × { x : V // x ∈ X } | ∀ (i : Fin r), -3 * ↑r ≤ Z i xx};
have nenI := ⋯;
let M := fun (x : { x : V // x ∈ X } × { x : V // x ∈ X }) => (Finset.image (τ x) Finset.univ).max' ⋯;
let c := ENNReal.ofReal (↑r * √(3 * ↑r));
ℙᵤ E < β →
(∀ (y : ℝ),
-1 ≤ y →
ℙᵤ (E ∩ {x : { x : V // x ∈ X } × { x : V // x ∈ X } | y ≤ M x}) < ENNReal.ofReal (Real.exp (-C.toReal * √(y + 1))) * β * ↑r) →
∫⁻ (x : { x : V // x ∈ X } × { x : V // x ∈ X }) in E, ENNReal.ofReal (Real.exp (∑ i : Fin r, √(Z i x + 3 * ↑r))) ∂ℙᵤ ≤ β * (↑r * c + 1)
theorem
expPos
{r : ℕ}
{V : Type}
[Fintype V]
[nenr : Nonempty (Fin r)]
{X : Finset V}
[Nonempty { x : V // x ∈ X }]
[MeasurableSpace { x : V // x ∈ X }]
[MeasurableSingletonClass ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[dm : DiscreteMeasurableSpace ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[DecidableEq { x : V // x ∈ X }]
{ℙᵤ : MeasureTheory.Measure ({ x : V // x ∈ X } × { x : V // x ∈ X })}
[MeasureTheory.IsProbabilityMeasure ℙᵤ]
{σ : Fin r → { x : V // x ∈ X } → V → ℝ}
:
let τ := fun (x : { x : V // x ∈ X } × { x : V // x ∈ X }) (i : Fin r) => σ i x.1 ⬝ᵥ σ i x.2;
let 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
juicy
{r : ℕ}
{V : Type}
[Fintype V]
[nenr : Nonempty (Fin r)]
{X : Finset V}
[Nonempty { x : V // x ∈ X }]
[MeasurableSpace { x : V // x ∈ X }]
[MeasurableSingletonClass ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[dm : DiscreteMeasurableSpace ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[DecidableEq { x : V // x ∈ X }]
{ℙᵤ : MeasureTheory.Measure ({ x : V // x ∈ X } × { x : V // x ∈ X })}
[MeasureTheory.IsProbabilityMeasure ℙᵤ]
{σ : Fin r → { x : V // x ∈ X } → V → ℝ}
:
let β := 3 ^ (-4 * ↑r);
let C := 4 * ↑r * √↑r;
let τ := fun (x : { x : V // x ∈ X } × { x : V // x ∈ X }) (i : Fin r) => σ i x.1 ⬝ᵥ σ i x.2;
let Z := fun (i : Fin r) (x : { x : V // x ∈ X } × { x : V // x ∈ X }) => 3 * ↑r * τ x i;
let E := {xx : { x : V // x ∈ X } × { x : V // x ∈ X } | ∀ (i : Fin r), -3 * ↑r ≤ Z i xx};
ℙᵤ.real E < β →
∃ (Λ : ℝ),
-1 ≤ Λ ∧ ∃ (i : Fin r),
ENNReal.ofReal (β * Real.exp (-C * √(Λ + 1))) ≤ ℙᵤ {x : { x : V // x ∈ X } × { x : V // x ∈ X } | Λ ≤ τ x i ∧ ∀ (j : Fin r), j ≠ i → -1 ≤ τ x j}
theorem
geometric
{r : ℕ}
{V : Type}
[Fintype V]
[nenr : Nonempty (Fin r)]
(X : Finset V)
[Nonempty { x : V // x ∈ X }]
[MeasurableSpace { x : V // x ∈ X }]
[MeasurableSingletonClass ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[dm : DiscreteMeasurableSpace ({ x : V // x ∈ X } × { x : V // x ∈ X })]
[DecidableEq { x : V // x ∈ X }]
(ℙᵤ : MeasureTheory.Measure ({ x : V // x ∈ X } × { x : V // x ∈ X }))
[MeasureTheory.IsProbabilityMeasure ℙᵤ]
(σ : Fin r → { x : V // x ∈ X } → V → ℝ)
:
let β := 3 ^ (-4 * ↑r);
let C := 4 * ↑r * √↑r;
let τ := fun (x : { x : V // x ∈ X } × { x : V // x ∈ X }) (i : Fin r) => σ i x.1 ⬝ᵥ σ i x.2;
∃ (Λ : ℝ),
-1 ≤ Λ ∧ ∃ (i : Fin r),
ENNReal.ofReal (β * Real.exp (-C * √(Λ + 1))) ≤ ℙᵤ {x : { x : V // x ∈ X } × { x : V // x ∈ X } | Λ ≤ τ x i ∧ ∀ (j : Fin r), j ≠ i → -1 ≤ τ x j}