-- Independent events
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Probability.Independence
import Conditional

-- Two events are independent when the probability of both is the product.
predicate IndependentEvents (P A B : Set) :=
  prob(P, A ∩ B) = (prob(P, A):R) * (prob(P, B):R)

theorem IndependentEvents.product (P A B : Set)
  requires independent : IndependentEvents(P, A, B)
  shows prob(P, A ∩ B) = (prob(P, A):R) * (prob(P, B):R)
proof
  unfold IndependentEvents at independent
  exact independent

theorem IndependentEvents.intro (P A B : Set)
  requires product : prob(P, A ∩ B) = (prob(P, A):R) * (prob(P, B):R)
  shows IndependentEvents(P, A, B)
proof
  unfold IndependentEvents
  exact product

theorem IndependentEvents.symmetric (Ω P A B : Set)
  requires space : ProbabilitySpace(Ω, P)
  requires eventA : A ⊆ Ω
  requires eventB : B ⊆ Ω
  requires independent : IndependentEvents(P, A, B)
  shows IndependentEvents(P, B, A)
proof
  have product := IndependentEvents.product with independent
  have realA := prob.real with space, eventA
  have realB := prob.real with space, eventB
  have commute := intersection.commutative at B, A
  have swap := realMulValue.commutative at prob(P, B), prob(P, A)
  unfold IndependentEvents
  rw [commute, product]
  symm
  exact swap

theorem IndependentEvents.whole_left (Ω P A : Set)
  requires space : ProbabilitySpace(Ω, P)
  requires eventA : A ⊆ Ω
  shows IndependentEvents(P, Ω, A)
proof
  have realA := prob.real with space, eventA
  have same := intersection.eq_right_of_subset at Ω, A with eventA
  have total := prob.whole with space
  unfold IndependentEvents
  rw [same, total]
  ring

theorem IndependentEvents.whole_right (Ω P A : Set)
  requires space : ProbabilitySpace(Ω, P)
  requires eventA : A ⊆ Ω
  shows IndependentEvents(P, A, Ω)
proof
  have whole := Subset.reflexive at Ω
  have left := IndependentEvents.whole_left with space, eventA
  exact IndependentEvents.symmetric with space, whole, eventA, left

theorem IndependentEvents.empty_left (Ω P A : Set)
  requires space : ProbabilitySpace(Ω, P)
  requires eventA : A ⊆ Ω
  shows IndependentEvents(P, ∅, A)
proof
  have realA := prob.real with space, eventA
  have same := intersection.left_empty at A
  have empty := prob.empty at P
  unfold IndependentEvents
  rw [same, empty]
  ring

theorem IndependentEvents.empty_right (Ω P A : Set)
  requires space : ProbabilitySpace(Ω, P)
  requires eventA : A ⊆ Ω
  shows IndependentEvents(P, A, ∅)
proof
  have empty := empty.subset at Ω
  have left := IndependentEvents.empty_left with space, eventA
  exact IndependentEvents.symmetric with space, empty, eventA, left

theorem IndependentEvents.complement_right (Ω P A B : Set)
  requires space : ProbabilitySpace(Ω, P)
  requires eventA : A ⊆ Ω
  requires eventB : B ⊆ Ω
  requires independent : IndependentEvents(P, A, B)
  shows IndependentEvents(P, A, Ω ∖ B)
proof
  have product := IndependentEvents.product with independent
  have realA := prob.real with space, eventA
  have realB := prob.real with space, eventB
  have same : A ∩ (Ω ∖ B) = A ∖ B
    ext y
    simp
  have split := prob.difference at Ω, P, A, B with space, eventA
  have complement := prob.complement with space, eventB
  unfold IndependentEvents
  rw [same, split, product, complement]
  ring

theorem IndependentEvents.complement_left (Ω P A B : Set)
  requires space : ProbabilitySpace(Ω, P)
  requires eventA : A ⊆ Ω
  requires eventB : B ⊆ Ω
  requires independent : IndependentEvents(P, A, B)
  shows IndependentEvents(P, Ω ∖ A, B)
proof
  have eventRest : Ω ∖ A ⊆ Ω by simp
  have swapped := IndependentEvents.symmetric with space, eventA, eventB,
      independent
  have complemented := IndependentEvents.complement_right with space, eventB,
      eventA, swapped
  exact IndependentEvents.symmetric with space, eventB, eventRest, complemented

theorem IndependentEvents.complement_both (Ω P A B : Set)
  requires space : ProbabilitySpace(Ω, P)
  requires eventA : A ⊆ Ω
  requires eventB : B ⊆ Ω
  requires independent : IndependentEvents(P, A, B)
  shows IndependentEvents(P, Ω ∖ A, Ω ∖ B)
proof
  have eventRest : Ω ∖ B ⊆ Ω by simp
  have right := IndependentEvents.complement_right with space, eventA, eventB,
      independent
  exact IndependentEvents.complement_left with space, eventA, eventRest, right

-- Independence means that conditioning on B does not change the odds of A.
theorem IndependentEvents.condProb (Ω P A B : Set)
  requires space : ProbabilitySpace(Ω, P)
  requires eventA : A ⊆ Ω
  requires eventB : B ⊆ Ω
  requires positive : (0:R) < (prob(P, B):R)
  requires independent : IndependentEvents(P, A, B)
  shows condProb(P, A, B) = prob(P, A)
proof
  have product := IndependentEvents.product with independent
  have realA := prob.real with space, eventA
  have realB := prob.real with space, eventB
  have nonzero := prob.ne_zero_of_positive with space, eventB, positive
  have pull := realDiv.mul_numerator_left at prob(P, A), prob(P, B), prob(P, B)
  have self := realDiv.self at prob(P, B) with nonzero
  have one := realMulValue.one_right at prob(P, A)
  rw [condProb.value, product, pull, self]
  exact one

theorem IndependentEvents.of_condProb (Ω P A B : Set)
  requires space : ProbabilitySpace(Ω, P)
  requires eventA : A ⊆ Ω
  requires eventB : B ⊆ Ω
  requires positive : (0:R) < (prob(P, B):R)
  requires conditioned : condProb(P, A, B) = prob(P, A)
  shows IndependentEvents(P, A, B)
proof
  have product := condProb.multiplication with space, eventA, eventB, positive
  rw conditioned at product
  exact IndependentEvents.intro with product

theorem IndependentEvents.of_prob_zero (Ω P A B : Set)
  requires space : ProbabilitySpace(Ω, P)
  requires eventA : A ⊆ Ω
  requires eventB : B ⊆ Ω
  requires zero : prob(P, A) = (0:R)
  shows IndependentEvents(P, A, B)
proof
  have eventMeet : A ∩ B ⊆ Ω by simp
  have realMeet := prob.real with space, eventMeet
  have realA := prob.real with space, eventA
  have realB := prob.real with space, eventB
  have upper := prob.intersection_le_left at Ω, P, A, B with space, eventA
  have lower := prob.nonnegative with space, eventMeet
  have vanishes : prob(P, A ∩ B) = (0:R) by linarith
  unfold IndependentEvents
  rw [vanishes, zero]
  ring

theorem IndependentEvents.of_prob_one (Ω P A B : Set)
  requires space : ProbabilitySpace(Ω, P)
  requires eventA : A ⊆ Ω
  requires eventB : B ⊆ Ω
  requires one : prob(P, A) = (1:R)
  shows IndependentEvents(P, A, B)
proof
  have eventMeet : A ∩ B ⊆ Ω by simp
  have eventRest : B ∖ A ⊆ Ω by simp
  have innerRest : B ∖ A ⊆ Ω ∖ A by simp
  have eventComplement : Ω ∖ A ⊆ Ω by simp
  have realA := prob.real with space, eventA
  have realMeet := prob.real with space, eventMeet
  have realRest := prob.real with space, eventRest
  have realComplement := prob.real with space, eventComplement
  have realB := prob.real with space, eventB
  have complement := prob.complement with space, eventA
  have bound := prob.monotone with space, eventComplement, innerRest
  have lower := prob.nonnegative with space, eventRest
  have split := prob.difference at Ω, P, B, A with space, eventB
  have commute := intersection.commutative at B, A
  rw commute at split
  have meetValue : prob(P, A ∩ B) = prob(P, B) by linarith
  unfold IndependentEvents
  rw [meetValue, one]
  ring

theorem IndependentEvents.union_left (Ω P A C B : Set)
  requires space : ProbabilitySpace(Ω, P)
  requires eventA : A ⊆ Ω
  requires eventC : C ⊆ Ω
  requires eventB : B ⊆ Ω
  requires disjoint : Disjoint(A, C)
  requires independentA : IndependentEvents(P, A, B)
  requires independentC : IndependentEvents(P, C, B)
  shows IndependentEvents(P, A ∪ C, B)
proof
  have productA := IndependentEvents.product with independentA
  have productC := IndependentEvents.product with independentC
  have realA := prob.real with space, eventA
  have realC := prob.real with space, eventC
  have realB := prob.real with space, eventB
  have eventMeetA : A ∩ B ⊆ Ω by simp
  have eventMeetC : C ∩ B ⊆ Ω by simp
  have split : (A ∪ C) ∩ B = (A ∩ B) ∪ (C ∩ B)
    ext y
    simp
  have innerC := intersection.subset_left at C, B
  have innerA := intersection.subset_left at A, B
  have disjointRight := Disjoint.of_subset_right with disjoint, innerC
  have disjointMeet := Disjoint.of_subset_left with disjointRight, innerA
  have union := prob.union_disjoint with space, eventMeetA, eventMeetC,
      disjointMeet
  have wholeUnion := prob.union_disjoint with space, eventA, eventC, disjoint
  unfold IndependentEvents
  rw [split, union, productA, productC, wholeUnion]
  ring

-- Three events, pairwise and mutually.
predicate PairwiseIndependent (P A B C : Set) :=
  IndependentEvents(P, A, B) ∧ IndependentEvents(P, A,
    C) ∧ IndependentEvents(P, B, C)

predicate MutuallyIndependent (P A B C : Set) :=
  PairwiseIndependent(P, A, B, C) ∧
    prob(P, A ∩ B ∩ C) = ((prob(P, A):R) * (prob(P, B):R)) * (prob(P, C):R)

theorem PairwiseIndependent.first (P A B C : Set)
  requires pairwise : PairwiseIndependent(P, A, B, C)
  shows IndependentEvents(P, A, B)
proof
  unfold PairwiseIndependent at pairwise
  exact pairwise.left

theorem PairwiseIndependent.second (P A B C : Set)
  requires pairwise : PairwiseIndependent(P, A, B, C)
  shows IndependentEvents(P, A, C)
proof
  unfold PairwiseIndependent at pairwise
  exact pairwise.right.left

theorem PairwiseIndependent.third (P A B C : Set)
  requires pairwise : PairwiseIndependent(P, A, B, C)
  shows IndependentEvents(P, B, C)
proof
  unfold PairwiseIndependent at pairwise
  exact pairwise.right.right

theorem PairwiseIndependent.swap (Ω P A B C : Set)
  requires space : ProbabilitySpace(Ω, P)
  requires eventA : A ⊆ Ω
  requires eventB : B ⊆ Ω
  requires pairwise : PairwiseIndependent(P, A, B, C)
  shows PairwiseIndependent(P, B, A, C)
proof
  have first := PairwiseIndependent.first with pairwise
  have second := PairwiseIndependent.second with pairwise
  have third := PairwiseIndependent.third with pairwise
  have swapped := IndependentEvents.symmetric with space, eventA, eventB, first
  unfold PairwiseIndependent
  refine ⟨swapped, third, second⟩

theorem MutuallyIndependent.pairwise (P A B C : Set)
  requires mutual : MutuallyIndependent(P, A, B, C)
  shows PairwiseIndependent(P, A, B, C)
proof
  unfold MutuallyIndependent at mutual
  exact mutual.left

theorem MutuallyIndependent.triple (P A B C : Set)
  requires mutual : MutuallyIndependent(P, A, B, C)
  shows prob(P, A ∩ B ∩ C) = ((prob(P, A):R) * (prob(P, B):R)) * (prob(P, C):R)
proof
  unfold MutuallyIndependent at mutual
  exact mutual.right

-- Under mutual independence the intersection A ∩ B is independent of C.
theorem MutuallyIndependent.intersection_left (P A B C : Set)
  requires mutual : MutuallyIndependent(P, A, B, C)
  shows IndependentEvents(P, A ∩ B, C)
proof
  have pairwise := MutuallyIndependent.pairwise with mutual
  have first := PairwiseIndependent.first with pairwise
  have productAB := IndependentEvents.product with first
  have triple := MutuallyIndependent.triple with mutual
  unfold IndependentEvents
  rw [triple, productAB]
  rfl