Theorem: Finset.exists_littlewood_offord_partition (LeanCamCombi/LittlewoodOfford.lean)

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 ∈ 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)
Tactic:
induction' s using Finset.induction with i s hi ih
State after:
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)

case insert
ι : 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,
    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)

State before:
case insert
ι : 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,
    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 ⟨P, hP, hs, hPr⟩ := ih fun j hj ↦ hf _ $ mem_insert_of_mem hj
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
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)

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
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)

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 _ _)
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)

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𝒜)
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)

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
State after:
no goals

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⟩
State after:
no goals

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
State after:
no goals