PO.ID.Partial.BalkePearl.Attainment
This module collects the explicit latent tables witnessing that each of the sixteen Balke-Pearl closed-form expressions is achieved by an observationally equivalent model, on the region of observed distributions where th
Basic 1 core · 1 supporting Observed cell probabilities form a distribution per instrument value ★ sum_cellProb_eq_one
Observed cell probabilities form a distribution per instrument value
lemma sum_cellProb_eq_one reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Under the Balke-Pearl IV base assumptions, for every instrument value z, the four observed outcome-treatment cell probabilities sum to one.
Formal statement
Proof (Lean source)
lemma sum_cellProb_eq_one (hA : S.BaseAssumptions) (z : Bool) :
∑ y : Bool, ∑ d : Bool, S.cellProb y d z = 1 := by
have h : ∀ y d, S.cellProb y d z = _ := fun y d => S.cellProb_eq_sum_latent hA y d z
have hs := S.latentProb_sum_eq_one
simp only [Fintype.sum_bool] at hs
simp only [Fintype.sum_bool, h]
cases z <;>
simp only [dArm, yArm, Fintype.sum_bool] <;>
norm_num <;>
linarith [hs]
1 supporting declaration (lemmas, instances)
-
cellProb_nonneglemma — Observed cell probabilities are nonnegative.Proof (Lean source)
lemma cellProb_nonneg (y d z : Bool) : 0 ≤ S.cellProb y d z := div_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg
Lower 15 core · 16 supporting Witnesses attaining the Balke-Pearl lower expressions ★ bpLower_mem_BPIdentifiedInterval
Witnesses attaining the Balke-Pearl lower expressions
def bpAux0t reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Free-variable choice t in the witness attaining bpLowerTerm 0.
def bpLowerWitness0 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Latent table attaining bpLowerTerm 0.
Definition (Lean source)
noncomputable def bpLowerWitness0 (S : POBalkePearlSystem P) :
Bool → Bool → Bool → Bool → ℝ
| false, false, false, false => S.cellProb false false true
| false, false, true, false => S.cellProb false false false - S.cellProb false false true -
S.cellProb false true true + S.cellProb true false false + S.bpAux0t
| false, true, false, false => S.cellProb false false false - S.cellProb false false true
| false, true, true, false => -S.cellProb false false false + S.cellProb false false true +
S.cellProb false true true - S.bpAux0t
| true, false, true, false => S.cellProb false true false - S.bpAux0t
| true, false, true, true => -S.cellProb false false false + S.cellProb false false true -
S.cellProb false true false + S.cellProb false true true - S.cellProb true false false +
S.cellProb true false true
| true, true, true, false => S.bpAux0t
| true, true, true, true => 1 - S.cellProb false false true - S.cellProb false true true -
S.cellProb true false true
| _, _, _, _ => 0
def bpAux1v reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Free-variable choice v in the witness attaining bpLowerTerm 1.
def bpLowerWitness1 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Latent table attaining bpLowerTerm 1.
Definition (Lean source)
noncomputable def bpLowerWitness1 (S : POBalkePearlSystem P) :
Bool → Bool → Bool → Bool → ℝ
| false, false, false, false => S.cellProb false false false
| false, false, true, false => -S.cellProb false false false + S.cellProb false false true -
S.cellProb false true false + S.cellProb true false true + S.bpAux1v
| false, true, true, false => S.cellProb false true true - S.bpAux1v
| false, true, true, true => S.cellProb false false false - S.cellProb false false true +
S.cellProb false true false - S.cellProb false true true + S.cellProb true false false -
S.cellProb true false true
| true, false, false, false => -S.cellProb false false false + S.cellProb false false true
| true, false, true, false => S.cellProb false false false - S.cellProb false false true +
S.cellProb false true false - S.bpAux1v
| true, true, true, false => S.bpAux1v
| true, true, true, true => 1 - S.cellProb false false false - S.cellProb false true false -
S.cellProb true false false
| _, _, _, _ => 0
def bpAux2u reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Free-variable choice u in the witness attaining bpLowerTerm 2.
def bpAux2v reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Free-variable choice v in the witness attaining bpLowerTerm 2.
def bpLowerWitness2 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Latent table attaining bpLowerTerm 2.
Definition (Lean source)
noncomputable def bpLowerWitness2 (S : POBalkePearlSystem P) :
Bool → Bool → Bool → Bool → ℝ
| false, false, false, false => S.cellProb false false false
| false, false, true, false => -S.cellProb false true true + S.cellProb true false false +
S.bpAux2v
| false, true, true, false => S.cellProb false true true - S.bpAux2v
| true, false, false, false => S.cellProb false true false - S.cellProb false true true +
S.cellProb true false false - S.cellProb true false true + S.bpAux2u
| true, false, false, true => -S.cellProb false false false + S.cellProb false false true -
S.cellProb false true false + S.cellProb false true true - S.cellProb true false false +
S.cellProb true false true - S.bpAux2u
| true, false, true, false => S.cellProb false true true - S.cellProb true false false +
S.cellProb true false true - S.bpAux2u - S.bpAux2v
| true, false, true, true => S.bpAux2u
| true, true, true, false => S.bpAux2v
| true, true, true, true => 1 - S.cellProb false false true - S.cellProb false true true -
S.cellProb true false true
| _, _, _, _ => 0
def bpAux3u reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Free-variable choice u in the witness attaining bpLowerTerm 3.
def bpAux3v reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Free-variable choice v in the witness attaining bpLowerTerm 3.
def bpLowerWitness3 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Latent table attaining bpLowerTerm 3.
Definition (Lean source)
noncomputable def bpLowerWitness3 (S : POBalkePearlSystem P) :
Bool → Bool → Bool → Bool → ℝ
| false, false, false, false => S.cellProb false false true
| false, false, true, false => -S.cellProb false true false + S.cellProb true false true +
S.bpAux3v
| false, true, false, false => -S.cellProb false true false + S.cellProb false true true -
S.cellProb true false false + S.cellProb true false true + S.bpAux3u
| false, true, false, true => S.cellProb false false false - S.cellProb false false true +
S.cellProb false true false - S.cellProb false true true + S.cellProb true false false -
S.cellProb true false true - S.bpAux3u
| false, true, true, false => S.cellProb false true false + S.cellProb true false false -
S.cellProb true false true - S.bpAux3u - S.bpAux3v
| false, true, true, true => S.bpAux3u
| true, false, true, false => S.cellProb false true false - S.bpAux3v
| true, true, true, false => S.bpAux3v
| true, true, true, true => 1 - S.cellProb false false false - S.cellProb false true false -
S.cellProb true false false
| _, _, _, _ => 0
def bpLowerWitness4 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Latent table attaining bpLowerTerm 4.
Definition (Lean source)
noncomputable def bpLowerWitness4 (S : POBalkePearlSystem P) :
Bool → Bool → Bool → Bool → ℝ
| false, false, false, false => S.cellProb false false false + S.cellProb false true false -
S.cellProb false true true + S.cellProb true false false
| false, true, false, false => -S.cellProb false true false + S.cellProb false true true -
S.cellProb true false false
| false, true, true, false => S.cellProb true false false
| true, false, false, true => -S.cellProb false false false + S.cellProb false false true -
S.cellProb false true false + S.cellProb false true true - S.cellProb true false false
| true, false, true, true => S.cellProb true false true
| true, true, true, false => S.cellProb false true false
| true, true, true, true => 1 - S.cellProb false false true - S.cellProb false true true -
S.cellProb true false true
| _, _, _, _ => 0
def bpLowerWitness5 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Latent table attaining bpLowerTerm 5.
Definition (Lean source)
noncomputable def bpLowerWitness5 (S : POBalkePearlSystem P) :
Bool → Bool → Bool → Bool → ℝ
| false, false, false, false => S.cellProb false false true
| false, false, true, false => S.cellProb true false false
| false, true, false, false => S.cellProb false true true
| false, true, false, true => S.cellProb false false false - S.cellProb false false true -
S.cellProb false true true
| true, false, true, false => S.cellProb false true false
| true, false, true, true => -S.cellProb false true false - S.cellProb true false false +
S.cellProb true false true
| true, true, true, true => 1 - S.cellProb false false false - S.cellProb true false true
| _, _, _, _ => 0
def bpLowerWitness6 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Latent table attaining bpLowerTerm 6.
Definition (Lean source)
noncomputable def bpLowerWitness6 (S : POBalkePearlSystem P) :
Bool → Bool → Bool → Bool → ℝ
| false, false, false, false => S.cellProb false false false
| false, false, true, false => S.cellProb true false true
| false, true, true, false => S.cellProb false true true
| false, true, true, true => -S.cellProb false true true + S.cellProb true false false -
S.cellProb true false true
| true, false, false, false => S.cellProb false true false
| true, false, false, true => -S.cellProb false false false + S.cellProb false false true -
S.cellProb false true false
| true, true, true, true => 1 - S.cellProb false false true - S.cellProb true false false
| _, _, _, _ => 0
def bpLowerWitness7 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Latent table attaining bpLowerTerm 7.
Definition (Lean source)
noncomputable def bpLowerWitness7 (S : POBalkePearlSystem P) :
Bool → Bool → Bool → Bool → ℝ
| false, false, false, false => S.cellProb false false true - S.cellProb false true false +
S.cellProb false true true + S.cellProb true false true
| false, true, false, true => S.cellProb false false false - S.cellProb false false true +
S.cellProb false true false - S.cellProb false true true - S.cellProb true false true
| false, true, true, true => S.cellProb true false false
| true, false, false, false => S.cellProb false true false - S.cellProb false true true -
S.cellProb true false true
| true, false, true, false => S.cellProb true false true
| true, true, true, false => S.cellProb false true true
| true, true, true, true => 1 - S.cellProb false false false - S.cellProb false true false -
S.cellProb true false false
| _, _, _, _ => 0
theorem bpLower_mem_BPIdentifiedInterval reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Under the Balke-Pearl IV base assumptions, the closed-form Balke-Pearl lower bound, computed from the observed cell probabilities, is itself attained as the average treatment effect of some feasible latent treatment-response table — it lies in the Balke-Pearl identified interval.
Formal statement
hypotheses
hA :
S.BaseAssumptions
conclusion
S.bpLower ∈ S.BPIdentifiedInterval hA
Proof (Lean source)
theorem bpLower_mem_BPIdentifiedInterval (hA : S.BaseAssumptions) :
S.bpLower ∈ S.BPIdentifiedInterval hA := by
have h₀ := S.latentProb_feasible hA
obtain ⟨i, -, hi⟩ :=
Finset.exists_mem_eq_sup' (Finset.univ_nonempty) S.bpLowerTerm
have hreg : ∀ j, S.bpLowerTerm j ≤ S.bpLowerTerm i := by
intro j
have h := Finset.le_sup' S.bpLowerTerm (Finset.mem_univ j)
rwa [hi] at h
have hb : S.bpLower = S.bpLowerTerm i := hi
rw [hb]
fin_cases i
· have h := PartialID.mem_identifiedInterval (obj := BPObjective)
(S.bpLowerWitness0_feasible hA h₀ hreg)
rw [S.bpLowerWitness0_objective hA] at h
exact h
· have h := PartialID.mem_identifiedInterval (obj := BPObjective)
(S.bpLowerWitness1_feasible hA h₀ hreg)
rw [S.bpLowerWitness1_objective hA] at h
exact h
· have h := PartialID.mem_identifiedInterval (obj := BPObjective)
(S.bpLowerWitness2_feasible hA h₀ hreg)
rw [S.bpLowerWitness2_objective hA] at h
exact h
· have h := PartialID.mem_identifiedInterval (obj := BPObjective)
(S.bpLowerWitness3_feasible hA h₀ hreg)
rw [S.bpLowerWitness3_objective hA] at h
exact h
· have h := PartialID.mem_identifiedInterval (obj := BPObjective)
(S.bpLowerWitness4_feasible hA h₀ hreg)
rw [S.bpLowerWitness4_objective hA] at h
exact h
· have h := PartialID.mem_identifiedInterval (obj := BPObjective)
(S.bpLowerWitness5_feasible hA h₀ hreg)
rw [S.bpLowerWitness5_objective hA] at h
exact h
· have h := PartialID.mem_identifiedInterval (obj := BPObjective)
(S.bpLowerWitness6_feasible hA h₀ hreg)
rw [S.bpLowerWitness6_objective hA] at h
exact h
· have h := PartialID.mem_identifiedInterval (obj := BPObjective)
(S.bpLowerWitness7_feasible hA h₀ hreg)
rw [S.bpLowerWitness7_objective hA] at h
exact h
16 supporting declarations (lemmas, instances)
-
bpLowerWitness0_feasibletheorem — The witness for bpLowerTerm 0 is feasible on its optimality region.hypothesesconclusionBPFeasible S hA S.bpLowerWitness0Proof (Lean source)
theorem bpLowerWitness0_feasible (hA : S.BaseAssumptions) {π₀ : Bool → Bool → Bool → Bool → ℝ} (h₀ : BPFeasible S hA π₀) (hreg : ∀ j, S.bpLowerTerm j ≤ S.bpLowerTerm 0) : BPFeasible S hA S.bpLowerWitness0 := by have hs := h₀.sum_one have hn := h₀.nonneg have n0 := hn false false false false have n1 := hn false false false true have n2 := hn false false true false have n3 := hn false false true true have n4 := hn false true false false have n5 := hn false true false true have n6 := hn false true true false have n7 := hn false true true true have n8 := hn true false false false have n9 := hn true false false true have n10 := hn true false true false have n11 := hn true false true true have n12 := hn true true false false have n13 := hn true true false true have n14 := hn true true true false have n15 := hn true true true true have hm := h₀.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 have r0 := hreg 0; have r1 := hreg 1; have r2 := hreg 2; have r3 := hreg 3 have r4 := hreg 4; have r5 := hreg 5; have r6 := hreg 6; have r7 := hreg 7 simp only [bpLowerTerm] at r0 r1 r2 r3 r4 r5 r6 r7 simp only [e000, e100, e010, e110, e001, e101, e011, e111] at r0 r1 r2 r3 r4 r5 r6 r7 rcases max_cases (0:ℝ) (S.cellProb false false true + S.cellProb false true true - S.cellProb false false false - S.cellProb true false false ) with ⟨hmx0, hmc0⟩ | ⟨hmx0, hmc0⟩ all_goals refine ⟨?_, ?_, ?_⟩ · rintro (_|_) (_|_) (_|_) (_|_) <;> simp only [bpLowerWitness0, bpAux0t, hmx0] <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith · simp only [bpLowerWitness0, bpAux0t, hmx0, Fintype.sum_bool] try simp only [e000, e100, e010, e110, e001, e101, e011, e111] linarith · rintro (_|_) (_|_) (_|_) <;> simp only [bpLowerWitness0, bpAux0t, hmx0, dArm, yArm, Fintype.sum_bool] <;> norm_num <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith -
bpLowerWitness0_objectivetheorem — The witness for bpLowerTerm 0 attains it.Proof (Lean source)
theorem bpLowerWitness0_objective (hA : S.BaseAssumptions) : BPObjective S.bpLowerWitness0 = S.bpLowerTerm 0 := by have h0 := S.sum_cellProb_eq_one hA false have h1 := S.sum_cellProb_eq_one hA true simp only [Fintype.sum_bool] at h0 h1 simp only [BPObjective, bpLowerWitness0, bpAux0t, bpLowerTerm, Fintype.sum_bool, boolToReal] linarith -
bpLowerWitness1_feasibletheorem — The witness for bpLowerTerm 1 is feasible on its optimality region.hypothesesconclusionBPFeasible S hA S.bpLowerWitness1Proof (Lean source)
theorem bpLowerWitness1_feasible (hA : S.BaseAssumptions) {π₀ : Bool → Bool → Bool → Bool → ℝ} (h₀ : BPFeasible S hA π₀) (hreg : ∀ j, S.bpLowerTerm j ≤ S.bpLowerTerm 1) : BPFeasible S hA S.bpLowerWitness1 := by have hs := h₀.sum_one have hn := h₀.nonneg have n0 := hn false false false false have n1 := hn false false false true have n2 := hn false false true false have n3 := hn false false true true have n4 := hn false true false false have n5 := hn false true false true have n6 := hn false true true false have n7 := hn false true true true have n8 := hn true false false false have n9 := hn true false false true have n10 := hn true false true false have n11 := hn true false true true have n12 := hn true true false false have n13 := hn true true false true have n14 := hn true true true false have n15 := hn true true true true have hm := h₀.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 have r0 := hreg 0; have r1 := hreg 1; have r2 := hreg 2; have r3 := hreg 3 have r4 := hreg 4; have r5 := hreg 5; have r6 := hreg 6; have r7 := hreg 7 simp only [bpLowerTerm] at r0 r1 r2 r3 r4 r5 r6 r7 simp only [e000, e100, e010, e110, e001, e101, e011, e111] at r0 r1 r2 r3 r4 r5 r6 r7 rcases max_cases (0:ℝ) (S.cellProb false false false - S.cellProb false false true + S.cellProb false true false - S.cellProb true false true ) with ⟨hmx0, hmc0⟩ | ⟨hmx0, hmc0⟩ all_goals refine ⟨?_, ?_, ?_⟩ · rintro (_|_) (_|_) (_|_) (_|_) <;> simp only [bpLowerWitness1, bpAux1v, hmx0] <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith · simp only [bpLowerWitness1, bpAux1v, hmx0, Fintype.sum_bool] try simp only [e000, e100, e010, e110, e001, e101, e011, e111] linarith · rintro (_|_) (_|_) (_|_) <;> simp only [bpLowerWitness1, bpAux1v, hmx0, dArm, yArm, Fintype.sum_bool] <;> norm_num <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith -
bpLowerWitness1_objectivetheorem — The witness for bpLowerTerm 1 attains it.Proof (Lean source)
theorem bpLowerWitness1_objective (hA : S.BaseAssumptions) : BPObjective S.bpLowerWitness1 = S.bpLowerTerm 1 := by have h0 := S.sum_cellProb_eq_one hA false have h1 := S.sum_cellProb_eq_one hA true simp only [Fintype.sum_bool] at h0 h1 simp only [BPObjective, bpLowerWitness1, bpAux1v, bpLowerTerm, Fintype.sum_bool, boolToReal] linarith -
bpLowerWitness2_feasibletheorem — The witness for bpLowerTerm 2 is feasible on its optimality region.hypothesesconclusionBPFeasible S hA S.bpLowerWitness2Proof (Lean source)
theorem bpLowerWitness2_feasible (hA : S.BaseAssumptions) {π₀ : Bool → Bool → Bool → Bool → ℝ} (h₀ : BPFeasible S hA π₀) (hreg : ∀ j, S.bpLowerTerm j ≤ S.bpLowerTerm 2) : BPFeasible S hA S.bpLowerWitness2 := by have hs := h₀.sum_one have hn := h₀.nonneg have n0 := hn false false false false have n1 := hn false false false true have n2 := hn false false true false have n3 := hn false false true true have n4 := hn false true false false have n5 := hn false true false true have n6 := hn false true true false have n7 := hn false true true true have n8 := hn true false false false have n9 := hn true false false true have n10 := hn true false true false have n11 := hn true false true true have n12 := hn true true false false have n13 := hn true true false true have n14 := hn true true true false have n15 := hn true true true true have hm := h₀.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 have r0 := hreg 0; have r1 := hreg 1; have r2 := hreg 2; have r3 := hreg 3 have r4 := hreg 4; have r5 := hreg 5; have r6 := hreg 6; have r7 := hreg 7 simp only [bpLowerTerm] at r0 r1 r2 r3 r4 r5 r6 r7 simp only [e000, e100, e010, e110, e001, e101, e011, e111] at r0 r1 r2 r3 r4 r5 r6 r7 rcases max_cases (0:ℝ) (S.cellProb false true true - S.cellProb false true false - S.cellProb true false false + S.cellProb true false true ) with ⟨hmx0, hmc0⟩ | ⟨hmx0, hmc0⟩ all_goals rcases max_cases (0:ℝ) (S.cellProb false true true - S.cellProb true false false ) with ⟨hmx1, hmc1⟩ | ⟨hmx1, hmc1⟩ all_goals refine ⟨?_, ?_, ?_⟩ · rintro (_|_) (_|_) (_|_) (_|_) <;> simp only [bpLowerWitness2, bpAux2u, bpAux2v, hmx0, hmx1] <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith · simp only [bpLowerWitness2, bpAux2u, bpAux2v, hmx0, hmx1, Fintype.sum_bool] try simp only [e000, e100, e010, e110, e001, e101, e011, e111] linarith · rintro (_|_) (_|_) (_|_) <;> simp only [bpLowerWitness2, bpAux2u, bpAux2v, hmx0, hmx1, dArm, yArm, Fintype.sum_bool] <;> norm_num <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith -
bpLowerWitness2_objectivetheorem — The witness for bpLowerTerm 2 attains it.Proof (Lean source)
theorem bpLowerWitness2_objective (hA : S.BaseAssumptions) : BPObjective S.bpLowerWitness2 = S.bpLowerTerm 2 := by have h0 := S.sum_cellProb_eq_one hA false have h1 := S.sum_cellProb_eq_one hA true simp only [Fintype.sum_bool] at h0 h1 simp only [BPObjective, bpLowerWitness2, bpAux2u, bpAux2v, bpLowerTerm, Fintype.sum_bool, boolToReal] linarith -
bpLowerWitness3_feasibletheorem — The witness for bpLowerTerm 3 is feasible on its optimality region.hypothesesconclusionBPFeasible S hA S.bpLowerWitness3Proof (Lean source)
theorem bpLowerWitness3_feasible (hA : S.BaseAssumptions) {π₀ : Bool → Bool → Bool → Bool → ℝ} (h₀ : BPFeasible S hA π₀) (hreg : ∀ j, S.bpLowerTerm j ≤ S.bpLowerTerm 3) : BPFeasible S hA S.bpLowerWitness3 := by have hs := h₀.sum_one have hn := h₀.nonneg have n0 := hn false false false false have n1 := hn false false false true have n2 := hn false false true false have n3 := hn false false true true have n4 := hn false true false false have n5 := hn false true false true have n6 := hn false true true false have n7 := hn false true true true have n8 := hn true false false false have n9 := hn true false false true have n10 := hn true false true false have n11 := hn true false true true have n12 := hn true true false false have n13 := hn true true false true have n14 := hn true true true false have n15 := hn true true true true have hm := h₀.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 have r0 := hreg 0; have r1 := hreg 1; have r2 := hreg 2; have r3 := hreg 3 have r4 := hreg 4; have r5 := hreg 5; have r6 := hreg 6; have r7 := hreg 7 simp only [bpLowerTerm] at r0 r1 r2 r3 r4 r5 r6 r7 simp only [e000, e100, e010, e110, e001, e101, e011, e111] at r0 r1 r2 r3 r4 r5 r6 r7 rcases max_cases (0:ℝ) (S.cellProb false true false - S.cellProb false true true + S.cellProb true false false - S.cellProb true false true ) with ⟨hmx0, hmc0⟩ | ⟨hmx0, hmc0⟩ all_goals rcases max_cases (0:ℝ) (S.cellProb false true false - S.cellProb true false true ) with ⟨hmx1, hmc1⟩ | ⟨hmx1, hmc1⟩ all_goals refine ⟨?_, ?_, ?_⟩ · rintro (_|_) (_|_) (_|_) (_|_) <;> simp only [bpLowerWitness3, bpAux3u, bpAux3v, hmx0, hmx1] <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith · simp only [bpLowerWitness3, bpAux3u, bpAux3v, hmx0, hmx1, Fintype.sum_bool] try simp only [e000, e100, e010, e110, e001, e101, e011, e111] linarith · rintro (_|_) (_|_) (_|_) <;> simp only [bpLowerWitness3, bpAux3u, bpAux3v, hmx0, hmx1, dArm, yArm, Fintype.sum_bool] <;> norm_num <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith -
bpLowerWitness3_objectivetheorem — The witness for bpLowerTerm 3 attains it.Proof (Lean source)
theorem bpLowerWitness3_objective (hA : S.BaseAssumptions) : BPObjective S.bpLowerWitness3 = S.bpLowerTerm 3 := by have h0 := S.sum_cellProb_eq_one hA false have h1 := S.sum_cellProb_eq_one hA true simp only [Fintype.sum_bool] at h0 h1 simp only [BPObjective, bpLowerWitness3, bpAux3u, bpAux3v, bpLowerTerm, Fintype.sum_bool, boolToReal] linarith -
bpLowerWitness4_feasibletheorem — The witness for bpLowerTerm 4 is feasible on its optimality region.hypothesesconclusionBPFeasible S hA S.bpLowerWitness4Proof (Lean source)
theorem bpLowerWitness4_feasible (hA : S.BaseAssumptions) {π₀ : Bool → Bool → Bool → Bool → ℝ} (h₀ : BPFeasible S hA π₀) (hreg : ∀ j, S.bpLowerTerm j ≤ S.bpLowerTerm 4) : BPFeasible S hA S.bpLowerWitness4 := by have hs := h₀.sum_one have hn := h₀.nonneg have n0 := hn false false false false have n1 := hn false false false true have n2 := hn false false true false have n3 := hn false false true true have n4 := hn false true false false have n5 := hn false true false true have n6 := hn false true true false have n7 := hn false true true true have n8 := hn true false false false have n9 := hn true false false true have n10 := hn true false true false have n11 := hn true false true true have n12 := hn true true false false have n13 := hn true true false true have n14 := hn true true true false have n15 := hn true true true true have hm := h₀.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 have r0 := hreg 0; have r1 := hreg 1; have r2 := hreg 2; have r3 := hreg 3 have r4 := hreg 4; have r5 := hreg 5; have r6 := hreg 6; have r7 := hreg 7 simp only [bpLowerTerm] at r0 r1 r2 r3 r4 r5 r6 r7 simp only [e000, e100, e010, e110, e001, e101, e011, e111] at r0 r1 r2 r3 r4 r5 r6 r7 refine ⟨?_, ?_, ?_⟩ · rintro (_|_) (_|_) (_|_) (_|_) <;> simp only [bpLowerWitness4] <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith · simp only [bpLowerWitness4, Fintype.sum_bool] try simp only [e000, e100, e010, e110, e001, e101, e011, e111] linarith · rintro (_|_) (_|_) (_|_) <;> simp only [bpLowerWitness4, dArm, yArm, Fintype.sum_bool] <;> norm_num <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith -
bpLowerWitness4_objectivetheorem — The witness for bpLowerTerm 4 attains it.Proof (Lean source)
theorem bpLowerWitness4_objective (hA : S.BaseAssumptions) : BPObjective S.bpLowerWitness4 = S.bpLowerTerm 4 := by have h0 := S.sum_cellProb_eq_one hA false have h1 := S.sum_cellProb_eq_one hA true simp only [Fintype.sum_bool] at h0 h1 simp only [BPObjective, bpLowerWitness4, bpLowerTerm, Fintype.sum_bool, boolToReal] linarith -
bpLowerWitness5_feasibletheorem — The witness for bpLowerTerm 5 is feasible on its optimality region.hypothesesconclusionBPFeasible S hA S.bpLowerWitness5Proof (Lean source)
theorem bpLowerWitness5_feasible (hA : S.BaseAssumptions) {π₀ : Bool → Bool → Bool → Bool → ℝ} (h₀ : BPFeasible S hA π₀) (hreg : ∀ j, S.bpLowerTerm j ≤ S.bpLowerTerm 5) : BPFeasible S hA S.bpLowerWitness5 := by have hs := h₀.sum_one have hn := h₀.nonneg have n0 := hn false false false false have n1 := hn false false false true have n2 := hn false false true false have n3 := hn false false true true have n4 := hn false true false false have n5 := hn false true false true have n6 := hn false true true false have n7 := hn false true true true have n8 := hn true false false false have n9 := hn true false false true have n10 := hn true false true false have n11 := hn true false true true have n12 := hn true true false false have n13 := hn true true false true have n14 := hn true true true false have n15 := hn true true true true have hm := h₀.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 have r0 := hreg 0; have r1 := hreg 1; have r2 := hreg 2; have r3 := hreg 3 have r4 := hreg 4; have r5 := hreg 5; have r6 := hreg 6; have r7 := hreg 7 simp only [bpLowerTerm] at r0 r1 r2 r3 r4 r5 r6 r7 simp only [e000, e100, e010, e110, e001, e101, e011, e111] at r0 r1 r2 r3 r4 r5 r6 r7 refine ⟨?_, ?_, ?_⟩ · rintro (_|_) (_|_) (_|_) (_|_) <;> simp only [bpLowerWitness5] <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith · simp only [bpLowerWitness5, Fintype.sum_bool] try simp only [e000, e100, e010, e110, e001, e101, e011, e111] linarith · rintro (_|_) (_|_) (_|_) <;> simp only [bpLowerWitness5, dArm, yArm, Fintype.sum_bool] <;> norm_num <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith -
bpLowerWitness5_objectivetheorem — The witness for bpLowerTerm 5 attains it.Proof (Lean source)
theorem bpLowerWitness5_objective (hA : S.BaseAssumptions) : BPObjective S.bpLowerWitness5 = S.bpLowerTerm 5 := by have h0 := S.sum_cellProb_eq_one hA false have h1 := S.sum_cellProb_eq_one hA true simp only [Fintype.sum_bool] at h0 h1 simp only [BPObjective, bpLowerWitness5, bpLowerTerm, Fintype.sum_bool, boolToReal] linarith -
bpLowerWitness6_feasibletheorem — The witness for bpLowerTerm 6 is feasible on its optimality region.hypothesesconclusionBPFeasible S hA S.bpLowerWitness6Proof (Lean source)
theorem bpLowerWitness6_feasible (hA : S.BaseAssumptions) {π₀ : Bool → Bool → Bool → Bool → ℝ} (h₀ : BPFeasible S hA π₀) (hreg : ∀ j, S.bpLowerTerm j ≤ S.bpLowerTerm 6) : BPFeasible S hA S.bpLowerWitness6 := by have hs := h₀.sum_one have hn := h₀.nonneg have n0 := hn false false false false have n1 := hn false false false true have n2 := hn false false true false have n3 := hn false false true true have n4 := hn false true false false have n5 := hn false true false true have n6 := hn false true true false have n7 := hn false true true true have n8 := hn true false false false have n9 := hn true false false true have n10 := hn true false true false have n11 := hn true false true true have n12 := hn true true false false have n13 := hn true true false true have n14 := hn true true true false have n15 := hn true true true true have hm := h₀.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 have r0 := hreg 0; have r1 := hreg 1; have r2 := hreg 2; have r3 := hreg 3 have r4 := hreg 4; have r5 := hreg 5; have r6 := hreg 6; have r7 := hreg 7 simp only [bpLowerTerm] at r0 r1 r2 r3 r4 r5 r6 r7 simp only [e000, e100, e010, e110, e001, e101, e011, e111] at r0 r1 r2 r3 r4 r5 r6 r7 refine ⟨?_, ?_, ?_⟩ · rintro (_|_) (_|_) (_|_) (_|_) <;> simp only [bpLowerWitness6] <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith · simp only [bpLowerWitness6, Fintype.sum_bool] try simp only [e000, e100, e010, e110, e001, e101, e011, e111] linarith · rintro (_|_) (_|_) (_|_) <;> simp only [bpLowerWitness6, dArm, yArm, Fintype.sum_bool] <;> norm_num <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith -
bpLowerWitness6_objectivetheorem — The witness for bpLowerTerm 6 attains it.Proof (Lean source)
theorem bpLowerWitness6_objective (hA : S.BaseAssumptions) : BPObjective S.bpLowerWitness6 = S.bpLowerTerm 6 := by have h0 := S.sum_cellProb_eq_one hA false have h1 := S.sum_cellProb_eq_one hA true simp only [Fintype.sum_bool] at h0 h1 simp only [BPObjective, bpLowerWitness6, bpLowerTerm, Fintype.sum_bool, boolToReal] linarith -
bpLowerWitness7_feasibletheorem — The witness for bpLowerTerm 7 is feasible on its optimality region.hypothesesconclusionBPFeasible S hA S.bpLowerWitness7Proof (Lean source)
theorem bpLowerWitness7_feasible (hA : S.BaseAssumptions) {π₀ : Bool → Bool → Bool → Bool → ℝ} (h₀ : BPFeasible S hA π₀) (hreg : ∀ j, S.bpLowerTerm j ≤ S.bpLowerTerm 7) : BPFeasible S hA S.bpLowerWitness7 := by have hs := h₀.sum_one have hn := h₀.nonneg have n0 := hn false false false false have n1 := hn false false false true have n2 := hn false false true false have n3 := hn false false true true have n4 := hn false true false false have n5 := hn false true false true have n6 := hn false true true false have n7 := hn false true true true have n8 := hn true false false false have n9 := hn true false false true have n10 := hn true false true false have n11 := hn true false true true have n12 := hn true true false false have n13 := hn true true false true have n14 := hn true true true false have n15 := hn true true true true have hm := h₀.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 have r0 := hreg 0; have r1 := hreg 1; have r2 := hreg 2; have r3 := hreg 3 have r4 := hreg 4; have r5 := hreg 5; have r6 := hreg 6; have r7 := hreg 7 simp only [bpLowerTerm] at r0 r1 r2 r3 r4 r5 r6 r7 simp only [e000, e100, e010, e110, e001, e101, e011, e111] at r0 r1 r2 r3 r4 r5 r6 r7 refine ⟨?_, ?_, ?_⟩ · rintro (_|_) (_|_) (_|_) (_|_) <;> simp only [bpLowerWitness7] <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith · simp only [bpLowerWitness7, Fintype.sum_bool] try simp only [e000, e100, e010, e110, e001, e101, e011, e111] linarith · rintro (_|_) (_|_) (_|_) <;> simp only [bpLowerWitness7, dArm, yArm, Fintype.sum_bool] <;> norm_num <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith -
bpLowerWitness7_objectivetheorem — The witness for bpLowerTerm 7 attains it.Proof (Lean source)
theorem bpLowerWitness7_objective (hA : S.BaseAssumptions) : BPObjective S.bpLowerWitness7 = S.bpLowerTerm 7 := by have h0 := S.sum_cellProb_eq_one hA false have h1 := S.sum_cellProb_eq_one hA true simp only [Fintype.sum_bool] at h0 h1 simp only [BPObjective, bpLowerWitness7, bpLowerTerm, Fintype.sum_bool, boolToReal] linarith
Upper 15 core · 16 supporting Witnesses attaining the Balke-Pearl upper expressions ★ bpUpper_mem_BPIdentifiedInterval
Witnesses attaining the Balke-Pearl upper expressions
def bpUAux0u reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Free-variable choice in the witness attaining bpUpperTerm 0.
def bpUpperWitness0 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Latent table attaining bpUpperTerm 0.
Definition (Lean source)
noncomputable def bpUpperWitness0 (S : POBalkePearlSystem P) :
Bool → Bool → Bool → Bool → ℝ
| false, false, false, true => S.cellProb false false false +
S.cellProb false false true + S.cellProb false true true +
S.cellProb true false false + S.bpUAux0u - 1
| false, false, true, true => S.cellProb true false true
| false, true, false, true => -S.cellProb false false true -
S.cellProb false true true - S.cellProb true false false - S.bpUAux0u + 1
| false, true, true, true => S.cellProb true false false - S.cellProb true false true
| true, false, false, false => S.cellProb false true false -
S.cellProb false true true
| true, false, false, true => -S.cellProb false false false -
S.cellProb false true false - S.cellProb true false false - S.bpUAux0u + 1
| true, true, false, false => S.cellProb false true true
| true, true, false, true => S.bpUAux0u
| _, _, _, _ => 0
def bpUAux1u reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Free-variable choice in the witness attaining bpUpperTerm 1.
def bpUpperWitness1 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Latent table attaining bpUpperTerm 1.
Definition (Lean source)
noncomputable def bpUpperWitness1 (S : POBalkePearlSystem P) :
Bool → Bool → Bool → Bool → ℝ
| false, false, false, true => S.cellProb false false false +
S.cellProb false false true + S.cellProb false true false +
S.cellProb true false true + S.bpUAux1u - 1
| false, false, true, true => S.cellProb true false false
| false, true, false, false => -S.cellProb false true false +
S.cellProb false true true
| false, true, false, true => -S.cellProb false false true -
S.cellProb false true true - S.cellProb true false true - S.bpUAux1u + 1
| true, false, false, true => -S.cellProb false false false -
S.cellProb false true false - S.cellProb true false true - S.bpUAux1u + 1
| true, false, true, true => -S.cellProb true false false + S.cellProb true false true
| true, true, false, false => S.cellProb false true false
| true, true, false, true => S.bpUAux1u
| _, _, _, _ => 0
def bpUAux2u reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Free-variable choice in the witness attaining bpUpperTerm 2.
def bpUAux2v reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Free-variable choice in the witness attaining bpUpperTerm 2.
def bpUpperWitness2 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Latent table attaining bpUpperTerm 2.
Definition (Lean source)
noncomputable def bpUpperWitness2 (S : POBalkePearlSystem P) :
Bool → Bool → Bool → Bool → ℝ
| false, false, false, true => S.cellProb false false false +
S.cellProb false false true + S.cellProb false true false +
S.cellProb true false false + S.bpUAux2v - 1
| false, false, true, true => S.cellProb true false true
| false, true, false, false => -S.cellProb false true false +
S.cellProb false true true - S.cellProb true false false +
S.cellProb true false true + S.bpUAux2u
| false, true, false, true => -S.cellProb false false true -
S.cellProb false true true - S.cellProb true false true - S.bpUAux2u - S.bpUAux2v
+ 1
| false, true, true, false => S.cellProb true false false - S.cellProb true false true
- S.bpUAux2u
| false, true, true, true => S.bpUAux2u
| true, false, false, true => -S.cellProb false false false -
S.cellProb false true false - S.cellProb true false false - S.bpUAux2v + 1
| true, true, false, false => S.cellProb false true false
| true, true, false, true => S.bpUAux2v
| _, _, _, _ => 0
def bpUAux3u reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Free-variable choice in the witness attaining bpUpperTerm 3.
def bpUAux3v reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Free-variable choice in the witness attaining bpUpperTerm 3.
def bpUpperWitness3 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Latent table attaining bpUpperTerm 3.
Definition (Lean source)
noncomputable def bpUpperWitness3 (S : POBalkePearlSystem P) :
Bool → Bool → Bool → Bool → ℝ
| false, false, false, true => S.cellProb false false false +
S.cellProb false false true + S.cellProb false true true +
S.cellProb true false true + S.bpUAux3v - 1
| false, false, true, true => S.cellProb true false false
| false, true, false, true => -S.cellProb false false true -
S.cellProb false true true - S.cellProb true false true - S.bpUAux3v + 1
| true, false, false, false => S.cellProb false true false -
S.cellProb false true true + S.cellProb true false false -
S.cellProb true false true + S.bpUAux3u
| true, false, false, true => -S.cellProb false false false -
S.cellProb false true false - S.cellProb true false false - S.bpUAux3u -
S.bpUAux3v + 1
| true, false, true, false => -S.cellProb true false false +
S.cellProb true false true - S.bpUAux3u
| true, false, true, true => S.bpUAux3u
| true, true, false, false => S.cellProb false true true
| true, true, false, true => S.bpUAux3v
| _, _, _, _ => 0
def bpUpperWitness4 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Latent table attaining bpUpperTerm 4.
Definition (Lean source)
noncomputable def bpUpperWitness4 (S : POBalkePearlSystem P) :
Bool → Bool → Bool → Bool → ℝ
| false, false, true, true => S.cellProb false false true -
S.cellProb false true false + S.cellProb false true true +
S.cellProb true false true
| false, true, false, true => S.cellProb false false false
| false, true, true, true => -S.cellProb false false true +
S.cellProb false true false - S.cellProb false true true +
S.cellProb true false false - S.cellProb true false true
| true, false, false, false => S.cellProb false false true
| true, false, true, false => -S.cellProb false false true +
S.cellProb false true false - S.cellProb false true true
| true, true, false, false => S.cellProb false true true
| true, true, false, true => -S.cellProb false false false -
S.cellProb false true false - S.cellProb true false false + 1
| _, _, _, _ => 0
def bpUpperWitness5 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Latent table attaining bpUpperTerm 5.
Definition (Lean source)
noncomputable def bpUpperWitness5 (S : POBalkePearlSystem P) :
Bool → Bool → Bool → Bool → ℝ
| false, false, false, true => S.cellProb false false true
| false, false, true, true => S.cellProb true false false
| false, true, false, false => S.cellProb false false false +
S.cellProb false true true + S.cellProb true false true - 1
| false, true, false, true => -S.cellProb false false true -
S.cellProb false true true - S.cellProb true false true + 1
| true, false, true, false => S.cellProb false false false +
S.cellProb false true false + S.cellProb true false true - 1
| true, false, true, true => -S.cellProb false false false -
S.cellProb false true false - S.cellProb true false false + 1
| true, true, false, false => -S.cellProb false false false -
S.cellProb true false true + 1
| _, _, _, _ => 0
def bpUpperWitness6 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Latent table attaining bpUpperTerm 6.
Definition (Lean source)
noncomputable def bpUpperWitness6 (S : POBalkePearlSystem P) :
Bool → Bool → Bool → Bool → ℝ
| false, false, false, true => S.cellProb false false false
| false, false, true, true => S.cellProb true false true
| false, true, true, false => S.cellProb false false true + S.cellProb false true true
+ S.cellProb true false false - 1
| false, true, true, true => -S.cellProb false false true - S.cellProb false true true
- S.cellProb true false true + 1
| true, false, false, false => S.cellProb false false true +
S.cellProb false true false + S.cellProb true false false - 1
| true, false, false, true => -S.cellProb false false false -
S.cellProb false true false - S.cellProb true false false + 1
| true, true, false, false => -S.cellProb false false true -
S.cellProb true false false + 1
| _, _, _, _ => 0
def bpUpperWitness7 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Latent table attaining bpUpperTerm 7.
Definition (Lean source)
noncomputable def bpUpperWitness7 (S : POBalkePearlSystem P) :
Bool → Bool → Bool → Bool → ℝ
| false, false, true, true => S.cellProb false false false +
S.cellProb false true false - S.cellProb false true true +
S.cellProb true false false
| false, true, false, false => S.cellProb false false false
| false, true, true, false => -S.cellProb false false false -
S.cellProb false true false + S.cellProb false true true
| true, false, false, true => S.cellProb false false true
| true, false, true, true => -S.cellProb false false false -
S.cellProb false true false + S.cellProb false true true -
S.cellProb true false false + S.cellProb true false true
| true, true, false, false => S.cellProb false true false
| true, true, false, true => -S.cellProb false false true - S.cellProb false true true
- S.cellProb true false true + 1
| _, _, _, _ => 0
theorem bpUpper_mem_BPIdentifiedInterval reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
Under the Balke-Pearl IV base assumptions, the closed-form Balke-Pearl upper bound, computed from the observed cell probabilities, is itself attained as the average treatment effect of some feasible latent treatment-response table — it lies in the Balke-Pearl identified interval.
Formal statement
hypotheses
hA :
S.BaseAssumptions
conclusion
S.bpUpper ∈ S.BPIdentifiedInterval hA
Proof (Lean source)
theorem bpUpper_mem_BPIdentifiedInterval (hA : S.BaseAssumptions) :
S.bpUpper ∈ S.BPIdentifiedInterval hA := by
have h₀ := S.latentProb_feasible hA
obtain ⟨i, -, hi⟩ :=
Finset.exists_mem_eq_inf' (Finset.univ_nonempty) S.bpUpperTerm
have hreg : ∀ j, S.bpUpperTerm i ≤ S.bpUpperTerm j := by
intro j
have h := Finset.inf'_le S.bpUpperTerm (Finset.mem_univ j)
rwa [hi] at h
have hb : S.bpUpper = S.bpUpperTerm i := hi
rw [hb]
fin_cases i
· have h := PartialID.mem_identifiedInterval (obj := BPObjective)
(S.bpUpperWitness0_feasible hA h₀ hreg)
rw [S.bpUpperWitness0_objective hA] at h
exact h
· have h := PartialID.mem_identifiedInterval (obj := BPObjective)
(S.bpUpperWitness1_feasible hA h₀ hreg)
rw [S.bpUpperWitness1_objective hA] at h
exact h
· have h := PartialID.mem_identifiedInterval (obj := BPObjective)
(S.bpUpperWitness2_feasible hA h₀ hreg)
rw [S.bpUpperWitness2_objective hA] at h
exact h
· have h := PartialID.mem_identifiedInterval (obj := BPObjective)
(S.bpUpperWitness3_feasible hA h₀ hreg)
rw [S.bpUpperWitness3_objective hA] at h
exact h
· have h := PartialID.mem_identifiedInterval (obj := BPObjective)
(S.bpUpperWitness4_feasible hA h₀ hreg)
rw [S.bpUpperWitness4_objective hA] at h
exact h
· have h := PartialID.mem_identifiedInterval (obj := BPObjective)
(S.bpUpperWitness5_feasible hA h₀ hreg)
rw [S.bpUpperWitness5_objective hA] at h
exact h
· have h := PartialID.mem_identifiedInterval (obj := BPObjective)
(S.bpUpperWitness6_feasible hA h₀ hreg)
rw [S.bpUpperWitness6_objective hA] at h
exact h
· have h := PartialID.mem_identifiedInterval (obj := BPObjective)
(S.bpUpperWitness7_feasible hA h₀ hreg)
rw [S.bpUpperWitness7_objective hA] at h
exact h
16 supporting declarations (lemmas, instances)
-
bpUpperWitness0_feasibletheorem — The witness for bpUpperTerm 0 is feasible on its optimality region.hypothesesconclusionBPFeasible S hA S.bpUpperWitness0Proof (Lean source)
theorem bpUpperWitness0_feasible (hA : S.BaseAssumptions) {π₀ : Bool → Bool → Bool → Bool → ℝ} (h₀ : BPFeasible S hA π₀) (hreg : ∀ j, S.bpUpperTerm 0 ≤ S.bpUpperTerm j) : BPFeasible S hA S.bpUpperWitness0 := by have hs := h₀.sum_one have hn := h₀.nonneg have n0 := hn false false false false have n1 := hn false false false true have n2 := hn false false true false have n3 := hn false false true true have n4 := hn false true false false have n5 := hn false true false true have n6 := hn false true true false have n7 := hn false true true true have n8 := hn true false false false have n9 := hn true false false true have n10 := hn true false true false have n11 := hn true false true true have n12 := hn true true false false have n13 := hn true true false true have n14 := hn true true true false have n15 := hn true true true true have hm := h₀.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 have r0 := hreg 0; have r1 := hreg 1; have r2 := hreg 2; have r3 := hreg 3 have r4 := hreg 4; have r5 := hreg 5; have r6 := hreg 6; have r7 := hreg 7 simp only [bpUpperTerm] at r0 r1 r2 r3 r4 r5 r6 r7 simp only [e000, e100, e010, e110, e001, e101, e011, e111] at r0 r1 r2 r3 r4 r5 r6 r7 rcases max_cases (0:ℝ) (-S.cellProb false false false - S.cellProb false false true - S.cellProb false true true - S.cellProb true false false + 1) with ⟨hmx0, hmc0⟩ | ⟨hmx0, hmc0⟩ all_goals refine ⟨?_, ?_, ?_⟩ · rintro (_|_) (_|_) (_|_) (_|_) <;> simp only [bpUpperWitness0, bpUAux0u, hmx0] <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith · simp only [bpUpperWitness0, bpUAux0u, hmx0, Fintype.sum_bool] try simp only [e000, e100, e010, e110, e001, e101, e011, e111] linarith · rintro (_|_) (_|_) (_|_) <;> simp only [bpUpperWitness0, bpUAux0u, hmx0, dArm, yArm, Fintype.sum_bool] <;> norm_num <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith -
bpUpperWitness0_objectivetheorem — The witness for bpUpperTerm 0 attains it.Proof (Lean source)
theorem bpUpperWitness0_objective (hA : S.BaseAssumptions) : BPObjective S.bpUpperWitness0 = S.bpUpperTerm 0 := by have h0 := S.sum_cellProb_eq_one hA false have h1 := S.sum_cellProb_eq_one hA true simp only [Fintype.sum_bool] at h0 h1 simp only [BPObjective, bpUpperWitness0, bpUAux0u, bpUpperTerm, Fintype.sum_bool, boolToReal] linarith -
bpUpperWitness1_feasibletheorem — The witness for bpUpperTerm 1 is feasible on its optimality region.hypothesesconclusionBPFeasible S hA S.bpUpperWitness1Proof (Lean source)
theorem bpUpperWitness1_feasible (hA : S.BaseAssumptions) {π₀ : Bool → Bool → Bool → Bool → ℝ} (h₀ : BPFeasible S hA π₀) (hreg : ∀ j, S.bpUpperTerm 1 ≤ S.bpUpperTerm j) : BPFeasible S hA S.bpUpperWitness1 := by have hs := h₀.sum_one have hn := h₀.nonneg have n0 := hn false false false false have n1 := hn false false false true have n2 := hn false false true false have n3 := hn false false true true have n4 := hn false true false false have n5 := hn false true false true have n6 := hn false true true false have n7 := hn false true true true have n8 := hn true false false false have n9 := hn true false false true have n10 := hn true false true false have n11 := hn true false true true have n12 := hn true true false false have n13 := hn true true false true have n14 := hn true true true false have n15 := hn true true true true have hm := h₀.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 have r0 := hreg 0; have r1 := hreg 1; have r2 := hreg 2; have r3 := hreg 3 have r4 := hreg 4; have r5 := hreg 5; have r6 := hreg 6; have r7 := hreg 7 simp only [bpUpperTerm] at r0 r1 r2 r3 r4 r5 r6 r7 simp only [e000, e100, e010, e110, e001, e101, e011, e111] at r0 r1 r2 r3 r4 r5 r6 r7 rcases max_cases (0:ℝ) (-S.cellProb false false false - S.cellProb false false true - S.cellProb false true false - S.cellProb true false true + 1) with ⟨hmx0, hmc0⟩ | ⟨hmx0, hmc0⟩ all_goals refine ⟨?_, ?_, ?_⟩ · rintro (_|_) (_|_) (_|_) (_|_) <;> simp only [bpUpperWitness1, bpUAux1u, hmx0] <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith · simp only [bpUpperWitness1, bpUAux1u, hmx0, Fintype.sum_bool] try simp only [e000, e100, e010, e110, e001, e101, e011, e111] linarith · rintro (_|_) (_|_) (_|_) <;> simp only [bpUpperWitness1, bpUAux1u, hmx0, dArm, yArm, Fintype.sum_bool] <;> norm_num <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith -
bpUpperWitness1_objectivetheorem — The witness for bpUpperTerm 1 attains it.Proof (Lean source)
theorem bpUpperWitness1_objective (hA : S.BaseAssumptions) : BPObjective S.bpUpperWitness1 = S.bpUpperTerm 1 := by have h0 := S.sum_cellProb_eq_one hA false have h1 := S.sum_cellProb_eq_one hA true simp only [Fintype.sum_bool] at h0 h1 simp only [BPObjective, bpUpperWitness1, bpUAux1u, bpUpperTerm, Fintype.sum_bool, boolToReal] linarith -
bpUpperWitness2_feasibletheorem — The witness for bpUpperTerm 2 is feasible on its optimality region.hypothesesconclusionBPFeasible S hA S.bpUpperWitness2Proof (Lean source)
theorem bpUpperWitness2_feasible (hA : S.BaseAssumptions) {π₀ : Bool → Bool → Bool → Bool → ℝ} (h₀ : BPFeasible S hA π₀) (hreg : ∀ j, S.bpUpperTerm 2 ≤ S.bpUpperTerm j) : BPFeasible S hA S.bpUpperWitness2 := by have hs := h₀.sum_one have hn := h₀.nonneg have n0 := hn false false false false have n1 := hn false false false true have n2 := hn false false true false have n3 := hn false false true true have n4 := hn false true false false have n5 := hn false true false true have n6 := hn false true true false have n7 := hn false true true true have n8 := hn true false false false have n9 := hn true false false true have n10 := hn true false true false have n11 := hn true false true true have n12 := hn true true false false have n13 := hn true true false true have n14 := hn true true true false have n15 := hn true true true true have hm := h₀.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 have r0 := hreg 0; have r1 := hreg 1; have r2 := hreg 2; have r3 := hreg 3 have r4 := hreg 4; have r5 := hreg 5; have r6 := hreg 6; have r7 := hreg 7 simp only [bpUpperTerm] at r0 r1 r2 r3 r4 r5 r6 r7 simp only [e000, e100, e010, e110, e001, e101, e011, e111] at r0 r1 r2 r3 r4 r5 r6 r7 rcases max_cases (0:ℝ) (S.cellProb false true false - S.cellProb false true true + S.cellProb true false false - S.cellProb true false true ) with ⟨hmx0, hmc0⟩ | ⟨hmx0, hmc0⟩ all_goals rcases max_cases (0:ℝ) (-S.cellProb false false false - S.cellProb false false true - S.cellProb false true false - S.cellProb true false false + 1) with ⟨hmx1, hmc1⟩ | ⟨hmx1, hmc1⟩ all_goals refine ⟨?_, ?_, ?_⟩ · rintro (_|_) (_|_) (_|_) (_|_) <;> simp only [bpUpperWitness2, bpUAux2u, bpUAux2v, hmx0, hmx1] <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith · simp only [bpUpperWitness2, bpUAux2u, bpUAux2v, hmx0, hmx1, Fintype.sum_bool] try simp only [e000, e100, e010, e110, e001, e101, e011, e111] linarith · rintro (_|_) (_|_) (_|_) <;> simp only [bpUpperWitness2, bpUAux2u, bpUAux2v, hmx0, hmx1, dArm, yArm, Fintype.sum_bool] <;> norm_num <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith -
bpUpperWitness2_objectivetheorem — The witness for bpUpperTerm 2 attains it.Proof (Lean source)
theorem bpUpperWitness2_objective (hA : S.BaseAssumptions) : BPObjective S.bpUpperWitness2 = S.bpUpperTerm 2 := by have h0 := S.sum_cellProb_eq_one hA false have h1 := S.sum_cellProb_eq_one hA true simp only [Fintype.sum_bool] at h0 h1 simp only [BPObjective, bpUpperWitness2, bpUAux2u, bpUAux2v, bpUpperTerm, Fintype.sum_bool, boolToReal] linarith -
bpUpperWitness3_feasibletheorem — The witness for bpUpperTerm 3 is feasible on its optimality region.hypothesesconclusionBPFeasible S hA S.bpUpperWitness3Proof (Lean source)
theorem bpUpperWitness3_feasible (hA : S.BaseAssumptions) {π₀ : Bool → Bool → Bool → Bool → ℝ} (h₀ : BPFeasible S hA π₀) (hreg : ∀ j, S.bpUpperTerm 3 ≤ S.bpUpperTerm j) : BPFeasible S hA S.bpUpperWitness3 := by have hs := h₀.sum_one have hn := h₀.nonneg have n0 := hn false false false false have n1 := hn false false false true have n2 := hn false false true false have n3 := hn false false true true have n4 := hn false true false false have n5 := hn false true false true have n6 := hn false true true false have n7 := hn false true true true have n8 := hn true false false false have n9 := hn true false false true have n10 := hn true false true false have n11 := hn true false true true have n12 := hn true true false false have n13 := hn true true false true have n14 := hn true true true false have n15 := hn true true true true have hm := h₀.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 have r0 := hreg 0; have r1 := hreg 1; have r2 := hreg 2; have r3 := hreg 3 have r4 := hreg 4; have r5 := hreg 5; have r6 := hreg 6; have r7 := hreg 7 simp only [bpUpperTerm] at r0 r1 r2 r3 r4 r5 r6 r7 simp only [e000, e100, e010, e110, e001, e101, e011, e111] at r0 r1 r2 r3 r4 r5 r6 r7 rcases max_cases (0:ℝ) (-S.cellProb false true false + S.cellProb false true true - S.cellProb true false false + S.cellProb true false true ) with ⟨hmx0, hmc0⟩ | ⟨hmx0, hmc0⟩ all_goals rcases max_cases (0:ℝ) (-S.cellProb false false false - S.cellProb false false true - S.cellProb false true true - S.cellProb true false true + 1) with ⟨hmx1, hmc1⟩ | ⟨hmx1, hmc1⟩ all_goals refine ⟨?_, ?_, ?_⟩ · rintro (_|_) (_|_) (_|_) (_|_) <;> simp only [bpUpperWitness3, bpUAux3u, bpUAux3v, hmx0, hmx1] <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith · simp only [bpUpperWitness3, bpUAux3u, bpUAux3v, hmx0, hmx1, Fintype.sum_bool] try simp only [e000, e100, e010, e110, e001, e101, e011, e111] linarith · rintro (_|_) (_|_) (_|_) <;> simp only [bpUpperWitness3, bpUAux3u, bpUAux3v, hmx0, hmx1, dArm, yArm, Fintype.sum_bool] <;> norm_num <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith -
bpUpperWitness3_objectivetheorem — The witness for bpUpperTerm 3 attains it.Proof (Lean source)
theorem bpUpperWitness3_objective (hA : S.BaseAssumptions) : BPObjective S.bpUpperWitness3 = S.bpUpperTerm 3 := by have h0 := S.sum_cellProb_eq_one hA false have h1 := S.sum_cellProb_eq_one hA true simp only [Fintype.sum_bool] at h0 h1 simp only [BPObjective, bpUpperWitness3, bpUAux3u, bpUAux3v, bpUpperTerm, Fintype.sum_bool, boolToReal] linarith -
bpUpperWitness4_feasibletheorem — The witness for bpUpperTerm 4 is feasible on its optimality region.hypothesesconclusionBPFeasible S hA S.bpUpperWitness4Proof (Lean source)
theorem bpUpperWitness4_feasible (hA : S.BaseAssumptions) {π₀ : Bool → Bool → Bool → Bool → ℝ} (h₀ : BPFeasible S hA π₀) (hreg : ∀ j, S.bpUpperTerm 4 ≤ S.bpUpperTerm j) : BPFeasible S hA S.bpUpperWitness4 := by have hs := h₀.sum_one have hn := h₀.nonneg have n0 := hn false false false false have n1 := hn false false false true have n2 := hn false false true false have n3 := hn false false true true have n4 := hn false true false false have n5 := hn false true false true have n6 := hn false true true false have n7 := hn false true true true have n8 := hn true false false false have n9 := hn true false false true have n10 := hn true false true false have n11 := hn true false true true have n12 := hn true true false false have n13 := hn true true false true have n14 := hn true true true false have n15 := hn true true true true have hm := h₀.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 have r0 := hreg 0; have r1 := hreg 1; have r2 := hreg 2; have r3 := hreg 3 have r4 := hreg 4; have r5 := hreg 5; have r6 := hreg 6; have r7 := hreg 7 simp only [bpUpperTerm] at r0 r1 r2 r3 r4 r5 r6 r7 simp only [e000, e100, e010, e110, e001, e101, e011, e111] at r0 r1 r2 r3 r4 r5 r6 r7 refine ⟨?_, ?_, ?_⟩ · rintro (_|_) (_|_) (_|_) (_|_) <;> simp only [bpUpperWitness4] <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith · simp only [bpUpperWitness4, Fintype.sum_bool] try simp only [e000, e100, e010, e110, e001, e101, e011, e111] linarith · rintro (_|_) (_|_) (_|_) <;> simp only [bpUpperWitness4, dArm, yArm, Fintype.sum_bool] <;> norm_num <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith -
bpUpperWitness4_objectivetheorem — The witness for bpUpperTerm 4 attains it.Proof (Lean source)
theorem bpUpperWitness4_objective (hA : S.BaseAssumptions) : BPObjective S.bpUpperWitness4 = S.bpUpperTerm 4 := by have h0 := S.sum_cellProb_eq_one hA false have h1 := S.sum_cellProb_eq_one hA true simp only [Fintype.sum_bool] at h0 h1 simp only [BPObjective, bpUpperWitness4, bpUpperTerm, Fintype.sum_bool, boolToReal] linarith -
bpUpperWitness5_feasibletheorem — The witness for bpUpperTerm 5 is feasible on its optimality region.hypothesesconclusionBPFeasible S hA S.bpUpperWitness5Proof (Lean source)
theorem bpUpperWitness5_feasible (hA : S.BaseAssumptions) {π₀ : Bool → Bool → Bool → Bool → ℝ} (h₀ : BPFeasible S hA π₀) (hreg : ∀ j, S.bpUpperTerm 5 ≤ S.bpUpperTerm j) : BPFeasible S hA S.bpUpperWitness5 := by have hs := h₀.sum_one have hn := h₀.nonneg have n0 := hn false false false false have n1 := hn false false false true have n2 := hn false false true false have n3 := hn false false true true have n4 := hn false true false false have n5 := hn false true false true have n6 := hn false true true false have n7 := hn false true true true have n8 := hn true false false false have n9 := hn true false false true have n10 := hn true false true false have n11 := hn true false true true have n12 := hn true true false false have n13 := hn true true false true have n14 := hn true true true false have n15 := hn true true true true have hm := h₀.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 have r0 := hreg 0; have r1 := hreg 1; have r2 := hreg 2; have r3 := hreg 3 have r4 := hreg 4; have r5 := hreg 5; have r6 := hreg 6; have r7 := hreg 7 simp only [bpUpperTerm] at r0 r1 r2 r3 r4 r5 r6 r7 simp only [e000, e100, e010, e110, e001, e101, e011, e111] at r0 r1 r2 r3 r4 r5 r6 r7 refine ⟨?_, ?_, ?_⟩ · rintro (_|_) (_|_) (_|_) (_|_) <;> simp only [bpUpperWitness5] <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith · simp only [bpUpperWitness5, Fintype.sum_bool] try simp only [e000, e100, e010, e110, e001, e101, e011, e111] linarith · rintro (_|_) (_|_) (_|_) <;> simp only [bpUpperWitness5, dArm, yArm, Fintype.sum_bool] <;> norm_num <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith -
bpUpperWitness5_objectivetheorem — The witness for bpUpperTerm 5 attains it.Proof (Lean source)
theorem bpUpperWitness5_objective (hA : S.BaseAssumptions) : BPObjective S.bpUpperWitness5 = S.bpUpperTerm 5 := by have h0 := S.sum_cellProb_eq_one hA false have h1 := S.sum_cellProb_eq_one hA true simp only [Fintype.sum_bool] at h0 h1 simp only [BPObjective, bpUpperWitness5, bpUpperTerm, Fintype.sum_bool, boolToReal] linarith -
bpUpperWitness6_feasibletheorem — The witness for bpUpperTerm 6 is feasible on its optimality region.hypothesesconclusionBPFeasible S hA S.bpUpperWitness6Proof (Lean source)
theorem bpUpperWitness6_feasible (hA : S.BaseAssumptions) {π₀ : Bool → Bool → Bool → Bool → ℝ} (h₀ : BPFeasible S hA π₀) (hreg : ∀ j, S.bpUpperTerm 6 ≤ S.bpUpperTerm j) : BPFeasible S hA S.bpUpperWitness6 := by have hs := h₀.sum_one have hn := h₀.nonneg have n0 := hn false false false false have n1 := hn false false false true have n2 := hn false false true false have n3 := hn false false true true have n4 := hn false true false false have n5 := hn false true false true have n6 := hn false true true false have n7 := hn false true true true have n8 := hn true false false false have n9 := hn true false false true have n10 := hn true false true false have n11 := hn true false true true have n12 := hn true true false false have n13 := hn true true false true have n14 := hn true true true false have n15 := hn true true true true have hm := h₀.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 have r0 := hreg 0; have r1 := hreg 1; have r2 := hreg 2; have r3 := hreg 3 have r4 := hreg 4; have r5 := hreg 5; have r6 := hreg 6; have r7 := hreg 7 simp only [bpUpperTerm] at r0 r1 r2 r3 r4 r5 r6 r7 simp only [e000, e100, e010, e110, e001, e101, e011, e111] at r0 r1 r2 r3 r4 r5 r6 r7 refine ⟨?_, ?_, ?_⟩ · rintro (_|_) (_|_) (_|_) (_|_) <;> simp only [bpUpperWitness6] <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith · simp only [bpUpperWitness6, Fintype.sum_bool] try simp only [e000, e100, e010, e110, e001, e101, e011, e111] linarith · rintro (_|_) (_|_) (_|_) <;> simp only [bpUpperWitness6, dArm, yArm, Fintype.sum_bool] <;> norm_num <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith -
bpUpperWitness6_objectivetheorem — The witness for bpUpperTerm 6 attains it.Proof (Lean source)
theorem bpUpperWitness6_objective (hA : S.BaseAssumptions) : BPObjective S.bpUpperWitness6 = S.bpUpperTerm 6 := by have h0 := S.sum_cellProb_eq_one hA false have h1 := S.sum_cellProb_eq_one hA true simp only [Fintype.sum_bool] at h0 h1 simp only [BPObjective, bpUpperWitness6, bpUpperTerm, Fintype.sum_bool, boolToReal] linarith -
bpUpperWitness7_feasibletheorem — The witness for bpUpperTerm 7 is feasible on its optimality region.hypothesesconclusionBPFeasible S hA S.bpUpperWitness7Proof (Lean source)
theorem bpUpperWitness7_feasible (hA : S.BaseAssumptions) {π₀ : Bool → Bool → Bool → Bool → ℝ} (h₀ : BPFeasible S hA π₀) (hreg : ∀ j, S.bpUpperTerm 7 ≤ S.bpUpperTerm j) : BPFeasible S hA S.bpUpperWitness7 := by have hs := h₀.sum_one have hn := h₀.nonneg have n0 := hn false false false false have n1 := hn false false false true have n2 := hn false false true false have n3 := hn false false true true have n4 := hn false true false false have n5 := hn false true false true have n6 := hn false true true false have n7 := hn false true true true have n8 := hn true false false false have n9 := hn true false false true have n10 := hn true false true false have n11 := hn true false true true have n12 := hn true true false false have n13 := hn true true false true have n14 := hn true true true false have n15 := hn true true true true have hm := h₀.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 have r0 := hreg 0; have r1 := hreg 1; have r2 := hreg 2; have r3 := hreg 3 have r4 := hreg 4; have r5 := hreg 5; have r6 := hreg 6; have r7 := hreg 7 simp only [bpUpperTerm] at r0 r1 r2 r3 r4 r5 r6 r7 simp only [e000, e100, e010, e110, e001, e101, e011, e111] at r0 r1 r2 r3 r4 r5 r6 r7 refine ⟨?_, ?_, ?_⟩ · rintro (_|_) (_|_) (_|_) (_|_) <;> simp only [bpUpperWitness7] <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith · simp only [bpUpperWitness7, Fintype.sum_bool] try simp only [e000, e100, e010, e110, e001, e101, e011, e111] linarith · rintro (_|_) (_|_) (_|_) <;> simp only [bpUpperWitness7, dArm, yArm, Fintype.sum_bool] <;> norm_num <;> try simp only [e000, e100, e010, e110, e001, e101, e011, e111] all_goals linarith -
bpUpperWitness7_objectivetheorem — The witness for bpUpperTerm 7 attains it.Proof (Lean source)
theorem bpUpperWitness7_objective (hA : S.BaseAssumptions) : BPObjective S.bpUpperWitness7 = S.bpUpperTerm 7 := by have h0 := S.sum_cellProb_eq_one hA false have h1 := S.sum_cellProb_eq_one hA true simp only [Fintype.sum_bool] at h0 h1 simp only [BPObjective, bpUpperWitness7, bpUpperTerm, Fintype.sum_bool, boolToReal] linarith