internlm/Lean-Github huggingface dataset:
Theorem: Finset.exists_littlewood_offord_partition
Proof state before:
case insert.intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s✝ : Finset ι
f : ι → E
r : ℝ
inst✝ : DecidableEq ι
hr : 0 < r
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, r ≤ ‖f i‖) →
    ∃ P,
      P.parts.card = s.card.choose (s.card / 2) ∧
        (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s) ∧ ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
hf : ∀ i_1 ∈ insert i s, r ≤ ‖f i_1‖
P : Finpartition s.powerset
hP : P.parts.card = s.card.choose (s.card / 2)
hs : ∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s
hPr : ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
⊢ ∃ P,
    P.parts.card = (insert i s).card.choose ((insert i s).card / 2) ∧
      (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ insert i s) ∧
        ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
Tactic:
clear ih
Proof state after:
case insert.intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s✝ : Finset ι
f : ι → E
r : ℝ
inst✝ : DecidableEq ι
hr : 0 < r
i : ι
s : Finset ι
hi : i ∉ s
hf : ∀ i_1 ∈ insert i s, r ≤ ‖f i_1‖
P : Finpartition s.powerset
hP : P.parts.card = s.card.choose (s.card / 2)
hs : ∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s
hPr : ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
⊢ ∃ P,
    P.parts.card = (insert i s).card.choose ((insert i s).card / 2) ∧
      (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ insert i s) ∧
        ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
Theorem: Finset.exists_littlewood_offord_partition
Proof state before:
case insert.intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s✝ : Finset ι
f : ι → E
r : ℝ
inst✝ : DecidableEq ι
hr : 0 < r
i : ι
s : Finset ι
hi : i ∉ s
hf : ∀ i_1 ∈ insert i s, r ≤ ‖f i_1‖
P : Finpartition s.powerset
hP : P.parts.card = s.card.choose (s.card / 2)
hs : ∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s
hPr : ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
⊢ ∃ P,
    P.parts.card = (insert i s).card.choose ((insert i s).card / 2) ∧
      (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ insert i s) ∧
        ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
Tactic:
obtain ⟨g, hg, hgf⟩ :=
  exists_dual_vector ℝ (f i) (norm_pos_iff.1 $ hr.trans_le $ hf _ $ mem_insert_self _ _)
Proof state after:
case insert.intro.intro.intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s✝ : Finset ι
f : ι → E
r : ℝ
inst✝ : DecidableEq ι
hr : 0 < r
i : ι
s : Finset ι
hi : i ∉ s
hf : ∀ i_1 ∈ insert i s, r ≤ ‖f i_1‖
P : Finpartition s.powerset
hP : P.parts.card = s.card.choose (s.card / 2)
hs : ∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s
hPr : ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
g : E →L[ℝ] ℝ
hg : ‖g‖ = 1
hgf : g (f i) = ↑‖f i‖
⊢ ∃ P,
    P.parts.card = (insert i s).card.choose ((insert i s).card / 2) ∧
      (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ insert i s) ∧
        ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
Theorem: Finset.exists_littlewood_offord_partition
Proof state before:
case insert.intro.intro.intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s✝ : Finset ι
f : ι → E
r : ℝ
inst✝ : DecidableEq ι
hr : 0 < r
i : ι
s : Finset ι
hi : i ∉ s
hf : ∀ i_1 ∈ insert i s, r ≤ ‖f i_1‖
P : Finpartition s.powerset
hP : P.parts.card = s.card.choose (s.card / 2)
hs : ∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s
hPr : ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
g : E →L[ℝ] ℝ
hg : ‖g‖ = 1
hgf : g (f i) = ↑‖f i‖
⊢ ∃ P,
    P.parts.card = (insert i s).card.choose ((insert i s).card / 2) ∧
      (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ insert i s) ∧
        ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
Tactic:
choose t ht using fun 𝒜 (h𝒜 : 𝒜 ∈ P.parts) ↦
  Finset.exists_max_image _ (fun t ↦ g (∑ i in t, f i)) (P.nonempty_of_mem_parts h𝒜)
Proof state after:
case insert.intro.intro.intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s✝ : Finset ι
f : ι → E
r : ℝ
inst✝ : DecidableEq ι
hr : 0 < r
i : ι
s : Finset ι
hi : i ∉ s
hf : ∀ i_1 ∈ insert i s, r ≤ ‖f i_1‖
P : Finpartition s.powerset
hP : P.parts.card = s.card.choose (s.card / 2)
hs : ∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s
hPr : ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
g : E →L[ℝ] ℝ
hg : ‖g‖ = 1
hgf : g (f i) = ↑‖f i‖
t : (𝒜 : Finset (Finset ι)) → 𝒜 ∈ P.parts → Finset ι
ht : ∀ (𝒜 : Finset (Finset ι)) (h𝒜 : 𝒜 ∈ P.parts), t 𝒜 h𝒜 ∈ 𝒜 ∧ ∀ x' ∈ 𝒜, g (∑ i ∈ x', f i) ≤ g (∑ i ∈ t 𝒜 h𝒜, f i)
⊢ ∃ P,
    P.parts.card = (insert i s).card.choose ((insert i s).card / 2) ∧
      (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ insert i s) ∧
        ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
Theorem: Finset.exists_littlewood_offord_partition
Proof state before:
case insert.intro.intro.intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s✝ : Finset ι
f : ι → E
r : ℝ
inst✝ : DecidableEq ι
hr : 0 < r
i : ι
s : Finset ι
hi : i ∉ s
hf : ∀ i_1 ∈ insert i s, r ≤ ‖f i_1‖
P : Finpartition s.powerset
hP : P.parts.card = s.card.choose (s.card / 2)
hs : ∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s
hPr : ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
g : E →L[ℝ] ℝ
hg : ‖g‖ = 1
hgf : g (f i) = ↑‖f i‖
t : (𝒜 : Finset (Finset ι)) → 𝒜 ∈ P.parts → Finset ι
ht : ∀ (𝒜 : Finset (Finset ι)) (h𝒜 : 𝒜 ∈ P.parts), t 𝒜 h𝒜 ∈ 𝒜 ∧ ∀ x' ∈ 𝒜, g (∑ i ∈ x', f i) ≤ g (∑ i ∈ t 𝒜 h𝒜, f i)
⊢ ∃ P,
    P.parts.card = (insert i s).card.choose ((insert i s).card / 2) ∧
      (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ insert i s) ∧
        ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
Tactic:
sorry
Proof state after:
no goals
Theorem: Finset.exists_littlewood_offord_partition
Proof state before:
case empty
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s : Finset ι
f : ι → E
r : ℝ
inst✝ : DecidableEq ι
hr : 0 < r
hf : ∀ i ∈ ∅, r ≤ ‖f i‖
⊢ ∃ P,
    P.parts.card = ∅.card.choose (∅.card / 2) ∧
      (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ ∅) ∧ ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
Tactic:
exact ⟨Finpartition.indiscrete $ singleton_ne_empty _, by simp⟩
Proof state after:
no goals
Theorem: Finset.exists_littlewood_offord_partition
Proof state before:
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s : Finset ι
f : ι → E
r : ℝ
inst✝ : DecidableEq ι
hr : 0 < r
hf : ∀ i ∈ ∅, r ≤ ‖f i‖
⊢ (Finpartition.indiscrete ⋯).parts.card = ∅.card.choose (∅.card / 2) ∧
    (∀ 𝒜 ∈ (Finpartition.indiscrete ⋯).parts, ∀ t ∈ 𝒜, t ⊆ ∅) ∧
      ∀ 𝒜 ∈ (Finpartition.indiscrete ⋯).parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.card_le_of_forall_dist_sum_le
Proof state before:
ι : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s : Finset ι
f : ι → E
r : ℝ
hr : 0 < r
h𝒜 : ∀ t ∈ 𝒜, t ⊆ s
hf : ∀ i ∈ s, r ≤ ‖f i‖
h𝒜r : ∀ u ∈ 𝒜, ∀ v ∈ 𝒜, dist (∑ i ∈ u, f i) (∑ i ∈ v, f i) < r
⊢ 𝒜.card ≤ s.card.choose (s.card / 2)
Tactic:
obtain ⟨P, hP, _hs, hr⟩ := exists_littlewood_offord_partition hr hf
Proof state after:
case intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s : Finset ι
f : ι → E
r : ℝ
hr✝ : 0 < r
h𝒜 : ∀ t ∈ 𝒜, t ⊆ s
hf : ∀ i ∈ s, r ≤ ‖f i‖
h𝒜r : ∀ u ∈ 𝒜, ∀ v ∈ 𝒜, dist (∑ i ∈ u, f i) (∑ i ∈ v, f i) < r
P : Finpartition s.powerset
hP : P.parts.card = s.card.choose (s.card / 2)
_hs : ∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s
hr : ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
⊢ 𝒜.card ≤ s.card.choose (s.card / 2)
Theorem: Finset.card_le_of_forall_dist_sum_le
Proof state before:
case intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s : Finset ι
f : ι → E
r : ℝ
hr✝ : 0 < r
h𝒜 : ∀ t ∈ 𝒜, t ⊆ s
hf : ∀ i ∈ s, r ≤ ‖f i‖
h𝒜r : ∀ u ∈ 𝒜, ∀ v ∈ 𝒜, dist (∑ i ∈ u, f i) (∑ i ∈ v, f i) < r
P : Finpartition s.powerset
hP : P.parts.card = s.card.choose (s.card / 2)
_hs : ∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s
hr : ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
⊢ 𝒜.card ≤ s.card.choose (s.card / 2)
Tactic:
rw [← hP]
Proof state after:
case intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s : Finset ι
f : ι → E
r : ℝ
hr✝ : 0 < r
h𝒜 : ∀ t ∈ 𝒜, t ⊆ s
hf : ∀ i ∈ s, r ≤ ‖f i‖
h𝒜r : ∀ u ∈ 𝒜, ∀ v ∈ 𝒜, dist (∑ i ∈ u, f i) (∑ i ∈ v, f i) < r
P : Finpartition s.powerset
hP : P.parts.card = s.card.choose (s.card / 2)
_hs : ∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s
hr : ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
⊢ 𝒜.card ≤ P.parts.card
Theorem: Finset.card_le_of_forall_dist_sum_le
Proof state before:
case intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
𝒜 : Finset (Finset ι)
s : Finset ι
f : ι → E
r : ℝ
hr✝ : 0 < r
h𝒜 : ∀ t ∈ 𝒜, t ⊆ s
hf : ∀ i ∈ s, r ≤ ‖f i‖
h𝒜r : ∀ u ∈ 𝒜, ∀ v ∈ 𝒜, dist (∑ i ∈ u, f i) (∑ i ∈ v, f i) < r
P : Finpartition s.powerset
hP : P.parts.card = s.card.choose (s.card / 2)
_hs : ∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s
hr : ∀ 𝒜 ∈ P.parts, (↑𝒜).Pairwise fun u v => r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i)
t : Finset ι
ht : t ∈ 𝒜
⊢ ∃ b ∈ P.parts, (fun x x_1 => x ∈ x_1) t b
Tactic:
simpa only [exists_prop] using P.exists_mem (mem_powerset.2 $ h𝒜 _ ht)
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.ne_zero
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : Nonempty α
a : α
h : μ = 0
⊢ (PMF.bernoulli' p ⋯).toMeasure = 0
Tactic:
rw [← hX.map a, h, Measure.map_zero]
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.aemeasurable
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
⊢ AEMeasurable (fun ω => a ∈ X ω) μ
Tactic:
classical
have : (PMF.bernoulli' p hX.le_one).toMeasure ≠ 0 := NeZero.ne _
rw [← hX.map a, Measure.map] at this
refine' (Ne.dite_ne_right_iff fun hX' ↦ _).1 this
rw [Measure.mapₗ_ne_zero_iff hX'.measurable_mk]
haveI : Nonempty α := ⟨a⟩
exact hX.ne_zero
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.aemeasurable
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
⊢ AEMeasurable (fun ω => a ∈ X ω) μ
Tactic:
have : (PMF.bernoulli' p hX.le_one).toMeasure ≠ 0 := NeZero.ne _
Proof state after:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
this : (PMF.bernoulli' p ⋯).toMeasure ≠ 0
⊢ AEMeasurable (fun ω => a ∈ X ω) μ
Theorem: ProbabilityTheory.IsBernoulliSeq.aemeasurable
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
this : (PMF.bernoulli' p ⋯).toMeasure ≠ 0
⊢ AEMeasurable (fun ω => a ∈ X ω) μ
Tactic:
rw [← hX.map a, Measure.map] at this
Proof state after:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
this :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
⊢ AEMeasurable (fun ω => a ∈ X ω) μ
Theorem: ProbabilityTheory.IsBernoulliSeq.aemeasurable
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
this :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
⊢ AEMeasurable (fun ω => a ∈ X ω) μ
Tactic:
refine' (Ne.dite_ne_right_iff fun hX' ↦ _).1 this
Proof state after:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
this :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
hX' : AEMeasurable (fun ω => a ∈ X ω) μ
⊢ (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hX')) μ ≠ 0
Theorem: ProbabilityTheory.IsBernoulliSeq.aemeasurable
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
this :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
hX' : AEMeasurable (fun ω => a ∈ X ω) μ
⊢ (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hX')) μ ≠ 0
Tactic:
rw [Measure.mapₗ_ne_zero_iff hX'.measurable_mk]
Proof state after:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
this :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
hX' : AEMeasurable (fun ω => a ∈ X ω) μ
⊢ μ ≠ 0
Theorem: ProbabilityTheory.IsBernoulliSeq.aemeasurable
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
this :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
hX' : AEMeasurable (fun ω => a ∈ X ω) μ
⊢ μ ≠ 0
Tactic:
haveI : Nonempty α := ⟨a⟩
Proof state after:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
this✝ :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
hX' : AEMeasurable (fun ω => a ∈ X ω) μ
this : Nonempty α
⊢ μ ≠ 0
Theorem: ProbabilityTheory.IsBernoulliSeq.aemeasurable
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
this✝ :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
hX' : AEMeasurable (fun ω => a ∈ X ω) μ
this : Nonempty α
⊢ μ ≠ 0
Tactic:
exact hX.ne_zero
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.nullMeasurableSet
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
⊢ NullMeasurableSet {ω | a ∈ X ω} μ
Tactic:
rw [(by ext; simp : {ω | a ∈ X ω} = (fun ω ↦ a ∈ X ω) ⁻¹' {True})]
Proof state after:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
⊢ NullMeasurableSet ((fun ω => a ∈ X ω) ⁻¹' {True}) μ
Theorem: ProbabilityTheory.IsBernoulliSeq.nullMeasurableSet
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
⊢ NullMeasurableSet ((fun ω => a ∈ X ω) ⁻¹' {True}) μ
Tactic:
exact (hX.aemeasurable a).nullMeasurableSet_preimage MeasurableSpace.measurableSet_top
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.nullMeasurableSet
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
⊢ {ω | a ∈ X ω} = (fun ω => a ∈ X ω) ⁻¹' {True}
Tactic:
ext
Proof state after:
case h
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
x✝ : Ω
⊢ x✝ ∈ {ω | a ∈ X ω} ↔ x✝ ∈ (fun ω => a ∈ X ω) ⁻¹' {True}
Theorem: ProbabilityTheory.IsBernoulliSeq.nullMeasurableSet
Proof state before:
case h
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
x✝ : Ω
⊢ x✝ ∈ {ω | a ∈ X ω} ↔ x✝ ∈ (fun ω => a ∈ X ω) ⁻¹' {True}
Tactic:
simp
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.meas_apply
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
⊢ μ {ω | a ∈ X ω} = ↑p
Tactic:
rw [(_ : {ω | a ∈ X ω} = (fun ω ↦ a ∈ X ω) ⁻¹' {True}),
  ← Measure.map_apply_of_aemeasurable (hX.aemeasurable a) MeasurableSpace.measurableSet_top]
Proof state after:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
⊢ (Measure.map (fun ω => a ∈ X ω) μ) {True} = ↑p

α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
⊢ {ω | a ∈ X ω} = (fun ω => a ∈ X ω) ⁻¹' {True}
Theorem: ProbabilityTheory.IsBernoulliSeq.meas_apply
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
⊢ (Measure.map (fun ω => a ∈ X ω) μ) {True} = ↑p
Tactic:
simp [hX.map]
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.meas_apply
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
⊢ {ω | a ∈ X ω} = (fun ω => a ∈ X ω) ⁻¹' {True}
Tactic:
ext ω
Proof state after:
case h
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
ω : Ω
⊢ ω ∈ {ω | a ∈ X ω} ↔ ω ∈ (fun ω => a ∈ X ω) ⁻¹' {True}
Theorem: ProbabilityTheory.IsBernoulliSeq.meas_apply
Proof state before:
case h
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
ω : Ω
⊢ ω ∈ {ω | a ∈ X ω} ↔ ω ∈ (fun ω => a ∈ X ω) ⁻¹' {True}
Tactic:
simp
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
⊢ μ {ω | {a | a ∈ X ω} = ↑s} = ↑p ^ s.card * (1 - ↑p) ^ (card α - s.card)
Tactic:
simp_rw [ext_iff, setOf_forall]
Proof state after:
α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
⊢ μ (⋂ i, {x | i ∈ {a | a ∈ X x} ↔ i ∈ ↑s}) = ↑p ^ s.card * (1 - ↑p) ^ (card α - s.card)
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
⊢ μ (⋂ i, {x | i ∈ {a | a ∈ X x} ↔ i ∈ ↑s}) = ↑p ^ s.card * (1 - ↑p) ^ (card α - s.card)
Tactic:
rw [hX.iIndepFun.meas_iInter, ← s.prod_mul_prod_compl, Finset.prod_eq_pow_card,
  Finset.prod_eq_pow_card, Finset.card_compl]
Proof state after:
α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
⊢ ∀ a ∈ sᶜ, μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = 1 - ↑p

α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
⊢ ∀ a ∈ s, μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = ↑p

α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
⊢ ∀ (i : α), MeasurableSet {x | i ∈ {a | a ∈ X x} ↔ i ∈ ↑s}
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
⊢ ∀ (i : α), MeasurableSet {x | i ∈ {a | a ∈ X x} ↔ i ∈ ↑s}
Tactic:
rintro a
Proof state after:
α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
a : α
⊢ MeasurableSet {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s}
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
a : α
⊢ MeasurableSet {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s}
Tactic:
by_cases a ∈ s
Proof state after:
case pos
α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∈ s
⊢ MeasurableSet {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s}

case neg
α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∉ s
⊢ MeasurableSet {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s}
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
⊢ ∀ a ∈ sᶜ, μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = 1 - ↑p
Tactic:
rintro a hi
Proof state after:
α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
a : α
hi : a ∈ sᶜ
⊢ μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = 1 - ↑p
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
a : α
hi : a ∈ sᶜ
⊢ μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = 1 - ↑p
Tactic:
rw [Finset.mem_compl] at hi
Proof state after:
α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
a : α
hi : a ∉ s
⊢ μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = 1 - ↑p
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
a : α
hi : a ∉ s
⊢ μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = 1 - ↑p
Tactic:
simp only [hi, ← compl_setOf, prob_compl_eq_one_sub₀, mem_setOf_eq, Finset.mem_coe,
  iff_false_iff, hX.nullMeasurableSet, hX.meas_apply]
Proof state after:
no goals