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
hypotheses
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.hypothesesconclusion0 ≤ S.cellProb y d zProof (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
For a potential-outcome system and its Balke--Pearl observational system, the first auxiliary free mass is , where denotes the observed probability of outcome and treatment at instrument value .
def bpLowerWitness0 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the latent-type witness table for the first lower-bound expression assigns its displayed mass to each of the eight listed latent profiles in the first case, second case, third case, fourth case, fifth case, sixth case, seventh case, and eighth case, and assigns zero in the remaining case.
Definition (Lean source)
parameters
S :
given by
clause 2
clause 4
clause 6
clause 8
clause 9
| _, _, _, _ => 0
def bpAux1v reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the second auxiliary free mass is , where is the observed outcome--treatment cell probability at instrument value .
def bpLowerWitness1 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the latent-type witness table for the second lower-bound expression assigns its displayed mass in the first, second, third, fourth, fifth, sixth, seventh, and eighth listed latent-profile cases, and zero otherwise.
Definition (Lean source)
parameters
S :
given by
clause 2
clause 4
clause 6
clause 8
clause 9
| _, _, _, _ => 0
def bpAux2u reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the first auxiliary free mass for the third lower-bound witness is , where is the observed outcome--treatment cell probability.
def bpAux2v reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the second auxiliary free mass for the third lower-bound witness is , where is the observed outcome--treatment cell probability.
def bpLowerWitness2 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the latent-type witness table for the third lower-bound expression assigns its displayed mass in the first, second, third, fourth, fifth, sixth, seventh, eighth, and ninth listed latent-profile cases, and zero otherwise.
Definition (Lean source)
parameters
S :
given by
clause 2
clause 4
clause 5
clause 6
clause 9
clause 10
| _, _, _, _ => 0
def bpAux3u reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the first auxiliary free mass for the fourth lower-bound witness is , where is the observed outcome--treatment cell probability.
def bpAux3v reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the second auxiliary free mass for the fourth lower-bound witness is , where is the observed outcome--treatment cell probability.
def bpLowerWitness3 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the latent-type witness table for the fourth lower-bound expression assigns its displayed mass in the first, second, third, fourth, fifth, sixth, seventh, eighth, and ninth listed latent-profile cases, and zero otherwise.
Definition (Lean source)
parameters
S :
given by
clause 2
clause 3
clause 4
clause 5
clause 9
clause 10
| _, _, _, _ => 0
def bpLowerWitness4 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the latent-type witness table for the fifth lower-bound expression assigns its displayed mass in the first, second, third, fourth, fifth, sixth, and seventh listed latent-profile cases, and zero otherwise.
Definition (Lean source)
parameters
S :
given by
clause 1
clause 2
clause 4
clause 7
clause 8
| _, _, _, _ => 0
def bpLowerWitness5 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the latent-type witness table for the sixth lower-bound expression assigns its displayed mass in the first, second, third, fourth, fifth, sixth, and seventh listed latent-profile cases, and zero otherwise.
Definition (Lean source)
parameters
S :
given by
clause 4
clause 6
clause 8
| _, _, _, _ => 0
def bpLowerWitness6 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the latent-type witness table for the seventh lower-bound expression assigns its displayed mass in the first, second, third, fourth, fifth, sixth, and seventh listed latent-profile cases, and zero otherwise.
Definition (Lean source)
parameters
S :
given by
clause 4
clause 6
clause 8
| _, _, _, _ => 0
def bpLowerWitness7 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the latent-type witness table for the eighth lower-bound expression assigns its displayed mass in the first, second, third, fourth, fifth, sixth, and seventh listed latent-profile cases, and zero otherwise.
Definition (Lean source)
parameters
S :
given by
clause 1
clause 2
clause 4
clause 7
clause 8
| _, _, _, _ => 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
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.hypothesesconclusionBPObjective S.bpLowerWitness0 = S.bpLowerTerm 0Proof (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.hypothesesconclusionBPObjective S.bpLowerWitness1 = S.bpLowerTerm 1Proof (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.hypothesesconclusionBPObjective S.bpLowerWitness2 = S.bpLowerTerm 2Proof (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.hypothesesconclusionBPObjective S.bpLowerWitness3 = S.bpLowerTerm 3Proof (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.hypothesesconclusionBPObjective S.bpLowerWitness4 = S.bpLowerTerm 4Proof (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.hypothesesconclusionBPObjective S.bpLowerWitness5 = S.bpLowerTerm 5Proof (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.hypothesesconclusionBPObjective S.bpLowerWitness6 = S.bpLowerTerm 6Proof (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.hypothesesconclusionBPObjective S.bpLowerWitness7 = S.bpLowerTerm 7Proof (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
For a potential-outcome system and its Balke--Pearl observational system, the first auxiliary free mass is , where denotes the observed probability of outcome and treatment at instrument value .
def bpUpperWitness0 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the latent-type witness table for the first upper-bound expression assigns its displayed mass in the first, second, third, fourth, fifth, sixth, seventh, and eighth listed latent-profile cases, and zero otherwise.
Definition (Lean source)
parameters
S :
given by
clause 1
clause 3
clause 6
clause 9
| _, _, _, _ => 0
def bpUAux1u reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the second auxiliary free mass is , where is the observed outcome--treatment cell probability.
def bpUpperWitness1 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the latent-type witness table for the second upper-bound expression assigns its displayed mass in the first, second, third, fourth, fifth, sixth, seventh, and eighth listed latent-profile cases, and zero otherwise.
Definition (Lean source)
parameters
S :
given by
clause 1
clause 4
clause 5
clause 9
| _, _, _, _ => 0
def bpUAux2u reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the first auxiliary free mass for the third upper-bound witness is , where is the observed outcome--treatment cell probability.
def bpUAux2v reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the second auxiliary free mass for the third upper-bound witness is , where is the observed outcome--treatment cell probability.
def bpUpperWitness2 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the latent-type witness table for the third upper-bound expression assigns its displayed mass in the first, second, third, fourth, fifth, sixth, seventh, eighth, and ninth listed latent-profile cases, and zero otherwise.
Definition (Lean source)
parameters
S :
given by
clause 1
clause 3
clause 4
clause 5
clause 7
clause 10
| _, _, _, _ => 0
def bpUAux3u reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the first auxiliary free mass for the fourth upper-bound witness is , where is the observed outcome--treatment cell probability.
def bpUAux3v reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the second auxiliary free mass for the fourth upper-bound witness is , where is the observed outcome--treatment cell probability.
def bpUpperWitness3 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the latent-type witness table for the fourth upper-bound expression assigns its displayed mass in the first, second, third, fourth, fifth, sixth, seventh, eighth, and ninth listed latent-profile cases, and zero otherwise.
Definition (Lean source)
parameters
S :
given by
clause 1
clause 3
clause 4
clause 5
clause 6
clause 10
| _, _, _, _ => 0
def bpUpperWitness4 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the latent-type witness table for the fifth upper-bound expression assigns its displayed mass in the first, second, third, fourth, fifth, sixth, and seventh listed latent-profile cases, and zero otherwise.
Definition (Lean source)
parameters
S :
given by
clause 1
clause 3
clause 5
clause 7
clause 8
| _, _, _, _ => 0
def bpUpperWitness5 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the latent-type witness table for the sixth upper-bound expression assigns its displayed mass in the first, second, third, fourth, fifth, sixth, and seventh listed latent-profile cases, and zero otherwise.
Definition (Lean source)
parameters
S :
given by
clause 3
clause 4
clause 5
clause 6
clause 8
| _, _, _, _ => 0
def bpUpperWitness6 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the latent-type witness table for the seventh upper-bound expression assigns its displayed mass in the first, second, third, fourth, fifth, sixth, and seventh listed latent-profile cases, and zero otherwise.
Definition (Lean source)
parameters
S :
given by
clause 3
clause 4
clause 5
clause 6
clause 8
| _, _, _, _ => 0
def bpUpperWitness7 reviewed
⚑ flagged
Causalean.PO.POBalkePearlSystem
For a potential-outcome system and its Balke--Pearl observational system, the latent-type witness table for the eighth upper-bound expression assigns its displayed mass in the first, second, third, fourth, fifth, sixth, and seventh listed latent-profile cases, and zero otherwise.
Definition (Lean source)
parameters
S :
given by
clause 1
clause 3
clause 5
clause 7
clause 8
| _, _, _, _ => 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
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.hypothesesconclusionBPObjective S.bpUpperWitness0 = S.bpUpperTerm 0Proof (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.hypothesesconclusionBPObjective S.bpUpperWitness1 = S.bpUpperTerm 1Proof (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.hypothesesconclusionBPObjective S.bpUpperWitness2 = S.bpUpperTerm 2Proof (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.hypothesesconclusionBPObjective S.bpUpperWitness3 = S.bpUpperTerm 3Proof (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.hypothesesconclusionBPObjective S.bpUpperWitness4 = S.bpUpperTerm 4Proof (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.hypothesesconclusionBPObjective S.bpUpperWitness5 = S.bpUpperTerm 5Proof (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.hypothesesconclusionBPObjective S.bpUpperWitness6 = S.bpUpperTerm 6Proof (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.hypothesesconclusionBPObjective S.bpUpperWitness7 = S.bpUpperTerm 7Proof (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