Panel.PO

theorem mobius_expansion [Fintype ι] (τ : (ι → Fin 2) → ℝ) (hτ0 : τ (fun _ => 0) = 0) (h : ι → Fin 2) : τ h = ∑ S ∈ (((Finset.univ : Finset ι).powerset.filter (·.Nonempty)) : Finset (Finset ι)), delta τ S * prod S (fun k => ((h k).val : ℝ)) := by classical let B : Finset ι := Finset.univ.filter (fun k => h k = 1) have hBmem : ∀ k, k ∈ B ↔ h k = 1 := by intro k simp [B, mem_filter] have hh_indB : h = indicator B := by funext k by_cases hk : k ∈ B · have hk' := (hBmem k).1 hk simp [indicator, hk, hk'] · have h0 : h k ≠ 1 := by intro hh exact hk ((hBmem k).2 hh) have h2 : h k = 0 := by apply Fin.ext have hval_ne : (h k).val ≠ 1 := by intro hv apply h0 apply Fin.ext simpa using hv omega simp [indicator, hk, h2] let u : Finset (Finset ι) := (Finset.univ : Finset ι).powerset.filter (·.Nonempty) let s : Finset (Finset ι) := B.powerset.filter (·.Nonempty) change τ h = ∑ S ∈ u, delta τ S * prod S (fun k => ((h k).val : ℝ)) have hstep1 : (∑ S ∈ u, delta τ S * prod S (fun k => ((h k).val : ℝ))) = ∑ S ∈ s, delta τ S := by have hmul : ∀ S ∈ u, delta τ S * prod S (fun k => ((h k).val : ℝ)) = if S ⊆ B then delta τ S else 0 := by intro S hS rw [prod_indicator_eq h B hBmem S] by_cases hSB : S ⊆ B <;> simp [hSB] rw [Finset.sum_congr rfl hmul] have hfilter : u.filter (fun S => S ⊆ B) = s := by ext S simp [u, s, and_comm] rw [← Finset.sum_filter] rw [hfilter] have hstep2 : (∑ S ∈ s, delta τ S) = ∑ A ∈ B.powerset, (∑ S ∈ s, if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) else 0) * τ (indicator A) := by rw [show s = B.powerset.filter (·.Nonempty) by rfl] calc (∑ S ∈ B.powerset.filter (·.Nonempty), delta τ S) = ∑ S ∈ B.powerset.filter (·.Nonempty), ∑ A ∈ B.powerset, if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) * τ (indicator A) else 0 := by refine Finset.sum_congr rfl ?_ intro S hS rw [delta] have hSsub : S ⊆ B := Finset.mem_powerset.mp (Finset.mem_filter.mp hS).1 have hcard : (∑ A ∈ S.powerset, (-1 : ℝ) ^ (S.card - A.card) * τ (indicator A)) = ∑ A ∈ B.powerset, if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) * τ (indicator A) else 0 := by rw [← Finset.sum_filter] have hPowEq : S.powerset = B.powerset.filter (fun A => A ⊆ S) := by ext A constructor · intro hAS exact Finset.mem_filter.mpr ⟨Finset.mem_powerset.mpr ((Finset.mem_powerset.mp hAS).trans hSsub), Finset.mem_powerset.mp hAS⟩ · intro hAS exact Finset.mem_powerset.mpr (Finset.mem_filter.mp hAS).2 simp [hPowEq] simp [hcard] _ = ∑ S ∈ B.powerset.filter (·.Nonempty), ∑ A ∈ B.powerset, (if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) else 0) * τ (indicator A) := by simp [ite_mul] _ = ∑ A ∈ B.powerset, ∑ S ∈ B.powerset.filter (·.Nonempty), (if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) else 0) * τ (indicator A) := by rw [Finset.sum_comm] _ = ∑ A ∈ B.powerset, (∑ S ∈ B.powerset.filter (·.Nonempty), if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) else 0) * τ (indicator A) := by simp [Finset.sum_mul] have hstep3 : (∑ A ∈ B.powerset, (∑ S ∈ s, if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) else 0) * τ (indicator A)) = τ (indicator B) := by have hterms : ∀ A ∈ B.powerset, (∑ S ∈ s, if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) else 0) * τ (indicator A) = if A = B then τ (indicator B) else 0 := by intro A hA by_cases hA0 : A = ∅ · subst hA0 by_cases hB0 : B = ∅ · rw [hB0] simp [hτ0] · have hne : (∅ : Finset ι) ≠ B := by intro h exact hB0 h.symm simp [hτ0, hne] · have hAne : A.Nonempty := Finset.nonempty_iff_ne_empty.mpr hA0 have hAS : A ⊆ B := Finset.mem_powerset.mp hA have hfilter : s.filter (fun S => A ⊆ S) = B.powerset.filter (A ⊆ ·) := by ext S constructor · intro hS rcases Finset.mem_filter.mp hS with ⟨hSs, hSA⟩ exact Finset.mem_filter.mpr ⟨(Finset.mem_filter.mp hSs).1, hSA⟩ · intro hS rcases Finset.mem_filter.mp hS with ⟨hSsub, hSA⟩ exact Finset.mem_filter.mpr ⟨Finset.mem_filter.mpr ⟨hSsub, hAne.mono hSA⟩, hSA⟩ have hinner : (∑ S ∈ s, if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) else 0) = ∑ S ∈ B.powerset.filter (A ⊆ ·), (-1 : ℝ) ^ (S.card - A.card) := by rw [← Finset.sum_filter] have hEq : s.filter (fun S => A ⊆ S) = B.powerset.filter (A ⊆ ·) := hfilter simp [hEq] rw [hinner] have hcoeff := coeff_sum A B hAS by_cases hABeq : A = B · subst hABeq simp [hcoeff] · simp [hcoeff, hABeq] calc (∑ A ∈ B.powerset, (∑ S ∈ s, if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) else 0) * τ (indicator A)) = ∑ A ∈ B.powerset, if A = B then τ (indicator B) else 0 := by exact Finset.sum_congr rfl hterms _ = τ (indicator B) := by rw [Finset.sum_eq_single B] · simp · intro A hA hAB simp [hAB] · intro hB simp at hB rw [hstep1, hstep2, hstep3] simp [hh_indB]

theorem mean_consistency (P : CellPartition μ ι) (i : ι) (Y Y0 Y1 : Ω → ℝ) {d : ℝ} (hd : d = 0 ∨ d = 1) (hcons : ∀ ω ∈ P.cell i, Y ω = Y0 ω + d * (Y1 ω - Y0 ω)) : P.mean Y i = P.mean Y0 i + d * (P.mean Y1 i - P.mean Y0 i) := by rcases hd with h0 | h1 · subst h0 have hY : P.mean Y i = P.mean Y0 i := P.mean_congr_on i (fun ω hω => by rw [hcons ω hω]; ring) rw [hY]; ring · subst h1 have hY : P.mean Y i = P.mean Y1 i := P.mean_congr_on i (fun ω hω => by rw [hcons ω hω]; ring) rw [hY]; ring

@[simp] lemma History_zero (a0 : A) (p : ℕ) (D : TreatmentPath I (Fin T₀) A) (i : I) (t : Fin T₀) : History a0 p D i t 0 = D i t := by unfold History simp