This file restarts the randomized lower bound for disjointness following the corrected proof in .codex/disjointness.txt.

The proof uses the textbook hard distribution: choose a special coordinate T; at T, sample independent bits (X_T, Y_T); away from T, sample one of (0,0), (1,0), (0,1) uniformly and independently. The information terms below are the corrected ones from (6.6):

• Alice: I(X_T : M | T, X_<T, Y_≥T, D).
• Bob: I(Y_T : M | T, X_≤T, Y_>T, D).

The old file used the wrong Y_≠T / X_≠T conditioning terms, which came from the typoed transcription and led to a different proof.

noncomputable instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.setFinFiniteMeasureSpace (n : ℕ+) : FiniteMeasureSpace (Set (Fin ↑n))

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.setFinFiniteMeasureSpace n = CommunicationComplexity.FiniteMeasureSpace.of (Set (Fin ↑n))

inductive CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.DisjointCoordinate : Type

The three possible disjoint coordinate-pairs used away from the special coordinate.

• neither : DisjointCoordinate
• leftOnly : DisjointCoordinate
• rightOnly : DisjointCoordinate

instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.instDecidableEqDisjointCoordinate : DecidableEq DisjointCoordinate

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.instDecidableEqDisjointCoordinate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.instFintypeDisjointCoordinate : Fintype DisjointCoordinate

Equations

• One or more equations did not get rendered due to their size.

instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCoordinateNonempty : Nonempty DisjointCoordinate

instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCoordinateMeasurableSpace : MeasurableSpace DisjointCoordinate

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCoordinateMeasurableSpace = ⊤

instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCoordinateDiscreteMeasurableSpace : DiscreteMeasurableSpace DisjointCoordinate

instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCoordinateFiniteMeasureSpace : FiniteMeasureSpace DisjointCoordinate

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.DisjointCoordinate.xBit : DisjointCoordinate → Bool

Alice's bit in a disjoint coordinate-pair.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.DisjointCoordinate.neither.xBit = false
• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.DisjointCoordinate.leftOnly.xBit = true
• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.DisjointCoordinate.rightOnly.xBit = false

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.DisjointCoordinate.yBit : DisjointCoordinate → Bool

Bob's bit in a disjoint coordinate-pair.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.DisjointCoordinate.neither.yBit = false
• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.DisjointCoordinate.leftOnly.yBit = false
• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.DisjointCoordinate.rightOnly.yBit = true

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.DisjointCoordinate.card : Fintype.card DisjointCoordinate = 3

There are three disjoint coordinate-pairs.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.DisjointCoordinate.not_xBit_and_yBit (c : DisjointCoordinate) : ¬(c.xBit = true ∧ c.yBit = true)

A disjoint coordinate-pair never has both bits equal to true.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.DisjointCoordinate.swap : DisjointCoordinate → DisjointCoordinate

Swap Alice's and Bob's sides in a disjoint coordinate.

Equations

• One or more equations did not get rendered due to their size.
• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.DisjointCoordinate.neither.swap = CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.DisjointCoordinate.neither

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.DisjointCoordinate.swap_swap (c : DisjointCoordinate) : c.swap.swap = c

Swapping sides twice recovers the original disjoint coordinate.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.DisjointCoordinate.xBit_swap (c : DisjointCoordinate) : c.swap.xBit = c.yBit

After swapping a disjoint coordinate, Alice sees Bob's original bit.

structure CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.HardSample (n : ℕ+) : Type

The sample space for the hard distribution. The other coordinate at T is ignored; keeping it in the sample space makes the ambient type a simple product-like finite type.

• T : Fin ↑n
• xT : Bool
• yT : Bool
• other : Fin ↑n → DisjointCoordinate

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.instDecidableEqHardSample.decEq {n✝ : ℕ+} (x✝ x✝¹ : HardSample n✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.instDecidableEqHardSample {n✝ : ℕ+} : DecidableEq (HardSample n✝)

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.instDecidableEqHardSample = CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.instDecidableEqHardSample.decEq

instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.instFintypeHardSample {n✝ : ℕ+} : Fintype (HardSample n✝)

Equations

• One or more equations did not get rendered due to their size.

instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.HardSample.instNonempty (n : ℕ+) : Nonempty (HardSample n)

instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.HardSample.instMeasurableSpace (n : ℕ+) : MeasurableSpace (HardSample n)

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.HardSample.instMeasurableSpace n = ⊤

noncomputable instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.HardSample.measureSpace (n : ℕ+) : MeasureTheory.MeasureSpace (HardSample n)

We use the uniform distribution on the explicit hard-distribution sample space.

Equations

• One or more equations did not get rendered due to their size.

instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.HardSample.isProbabilityMeasure (n : ℕ+) : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

noncomputable instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.HardSample.finiteProbabilitySpace (n : ℕ+) : FiniteProbabilitySpace (HardSample n)

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.HardSample.equivProd (n : ℕ+) : HardSample n ≃ Fin ↑n × Bool × Bool × (Fin ↑n → DisjointCoordinate)

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.HardSample.card (n : ℕ+) : Fintype.card (HardSample n) = ↑n * 4 * 3 ^ ↑n

Cardinality of the explicit hard-distribution sample space.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformFin (n : ℕ+) : MeasureTheory.ProbabilityMeasure (Fin ↑n)

Uniform law on the special coordinate.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformFin n = ⟨ProbabilityTheory.uniformOn Set.univ, ⋯⟩

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformFin_singleton (n : ℕ+) (i : Fin ↑n) : (↑(uniformFin n)).real {i} = 1 / ↑↑n

Each coordinate has mass 1 / n under the uniform law on Fin n.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformFin_real (n : ℕ+) (S : Set (Fin ↑n)) : (↑(uniformFin n)).real S = ↑(Fintype.card { i : Fin ↑n // i ∈ S }) / ↑↑n

The uniform law on Fin n assigns mass by normalized cardinality.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformFin_univ (n : ℕ+) : (↑(uniformFin n)).real Set.univ = 1

The uniform law on Fin n has total mass 1.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformBool : MeasureTheory.ProbabilityMeasure Bool

Uniform law on one bit.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformBool_singleton (b : Bool) : (↑uniformBool).real {b} = 1 / 2

Each bit has mass 1 / 2 under the uniform law on one bit.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformBool_real (S : Set Bool) : (↑uniformBool).real S = ↑(Fintype.card { b : Bool // b ∈ S }) / 2

The uniform law on Bool assigns mass by normalized cardinality.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformBool_univ : (↑uniformBool).real Set.univ = 1

The uniform law on Bool has total mass 1.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformDisjointCoordinateVector (n : ℕ+) : MeasureTheory.ProbabilityMeasure (Fin ↑n → DisjointCoordinate)

The uniform law on generated disjoint coordinate vectors.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformDisjointCoordinateVector n = ⟨ProbabilityTheory.uniformOn Set.univ, ⋯⟩

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformDisjointCoordinate : MeasureTheory.ProbabilityMeasure DisjointCoordinate

The uniform law on one disjoint coordinate.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformDisjointCoordinateVector_singleton (n : ℕ+) (coords : Fin ↑n → DisjointCoordinate) : (↑(uniformDisjointCoordinateVector n)).real {coords} = 1 / 3 ^ ↑n

Each generated disjoint coordinate vector has mass 3^{-n} under the uniform law.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformDisjointCoordinateVector_real (n : ℕ+) (S : Set (Fin ↑n → DisjointCoordinate)) : (↑(uniformDisjointCoordinateVector n)).real S = ↑(Fintype.card { coords : Fin ↑n → DisjointCoordinate // coords ∈ S }) / 3 ^ ↑n

The uniform law on disjoint-coordinate vectors assigns mass by normalized cardinality.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformDisjointCoordinateVector_univ (n : ℕ+) : (↑(uniformDisjointCoordinateVector n)).real Set.univ = 1

The uniform law on disjoint-coordinate vectors has total mass 1.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformDisjointCoordinate_singleton (c : DisjointCoordinate) : (↑uniformDisjointCoordinate).real {c} = 1 / 3

Each disjoint coordinate has mass 1 / 3 under the one-coordinate uniform law.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBit (n : ℕ+) (ω : HardSample n) (i : Fin ↑n) : Bool

Alice's bit at coordinate i under a hard-distribution sample.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBit n ω i = if i = ω.T then ω.xT else (ω.other i).xBit

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yBit (n : ℕ+) (ω : HardSample n) (i : Fin ↑n) : Bool

Bob's bit at coordinate i under a hard-distribution sample.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yBit n ω i = if i = ω.T then ω.yT else (ω.other i).yBit

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.X (n : ℕ+) (ω : HardSample n) : Set (Fin ↑n)

Alice's input set under a hard-distribution sample.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.X n ω = {i : Fin ↑n | CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBit n ω i = true}

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.Y (n : ℕ+) (ω : HardSample n) : Set (Fin ↑n)

Bob's input set under a hard-distribution sample.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.Y n ω = {i : Fin ↑n | CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yBit n ω i = true}

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xVector (n : ℕ+) (ω : HardSample n) : Fin ↑n → Bool

Alice's full input vector under a hard-distribution sample.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xVector n ω = CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBit n ω

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yVector (n : ℕ+) (ω : HardSample n) : Fin ↑n → Bool

Bob's full input vector under a hard-distribution sample.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yVector n ω = CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yBit n ω

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.reverseBoolVector (n : ℕ+) (v : Fin ↑n → Bool) : Fin ↑n → Bool

Reverse the coordinate order of a boolean vector.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.reverseBoolVector n v = v ∘ Fin.rev

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.reverseBoolVector_reverseBoolVector (n : ℕ+) (v : Fin ↑n → Bool) : reverseBoolVector n (reverseBoolVector n v) = v

Reversing a boolean vector twice recovers it.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.reverseBoolVector_injective (n : ℕ+) : Function.Injective (reverseBoolVector n)

Reversing boolean vectors is injective.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.reverseSet (n : ℕ+) (S : Set (Fin ↑n)) : Set (Fin ↑n)

Reverse the coordinate order of a subset of coordinates.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.reverseSet n S = {i : Fin ↑n | i.rev ∈ S}

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.reverseSet_reverseSet (n : ℕ+) (S : Set (Fin ↑n)) : reverseSet n (reverseSet n S) = S

Reversing a coordinate set twice recovers it.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.input (n : ℕ+) (ω : HardSample n) : Set (Fin ↑n) × Set (Fin ↑n)

The input pair generated by a hard-distribution sample.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialIntersect (n : ℕ+) : Set (HardSample n)

The event that the special coordinate is an actual intersection.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialBitsEvent (n : ℕ+) (bx bY : Bool) : Set (HardSample n)

The event that the two special-coordinate bits have prescribed values.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialCoordinateEvent (n : ℕ+) (i : Fin ↑n) : Set (HardSample n)

The event that the special coordinate has a prescribed value.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialCoordinateEvent n i = {ω : CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.HardSample n | ω.T = i}

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialZeroZero (n : ℕ+) : Set (HardSample n)

The event that both special-coordinate bits are zero.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialZeroZero n = CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialBitsEvent n false false

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointEvent (n : ℕ+) : Set (HardSample n)

The event that the generated input pair is disjoint.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialIntersectFintype (n : ℕ+) : Fintype { ω : HardSample n // ω ∈ specialIntersect n }

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialIntersectFintype n = id inferInstance

noncomputable instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialBitsEventFintype (n : ℕ+) (bx bY : Bool) : Fintype { ω : HardSample n // ω ∈ specialBitsEvent n bx bY }

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialBitsEventFintype n bx bY = id inferInstance

noncomputable instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialCoordinateEventFintype (n : ℕ+) (i : Fin ↑n) : Fintype { ω : HardSample n // ω ∈ specialCoordinateEvent n i }

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialCoordinateEventFintype n i = id inferInstance

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialCoordinate (n : ℕ+) (ω : HardSample n) : Fin ↑n

The special coordinate selected by the hard distribution.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialCoordinate n ω = ω.T

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialX (n : ℕ+) (ω : HardSample n) : Bool

Alice's bit at the special coordinate.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialX n ω = ω.xT

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialY (n : ℕ+) (ω : HardSample n) : Bool

Bob's bit at the special coordinate.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialY n ω = ω.yT

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBeforeSpecial (n : ℕ+) (ω : HardSample n) : Fin ↑n → Bool

Alice's input bits before the special coordinate, padded by false elsewhere.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBeforeSpecial n ω i = if i < ω.T then CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBit n ω i else false

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xLeSpecial (n : ℕ+) (ω : HardSample n) : Fin ↑n → Bool

Alice's input bits up to and including the special coordinate, padded by false elsewhere.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xLeSpecial n ω i = if i ≤ ω.T then CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBit n ω i else false

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yAfterSpecial (n : ℕ+) (ω : HardSample n) : Fin ↑n → Bool

Bob's input bits after the special coordinate, padded by false elsewhere.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yAfterSpecial n ω i = if ω.T < i then CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yBit n ω i else false

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yGeSpecial (n : ℕ+) (ω : HardSample n) : Fin ↑n → Bool

Bob's input bits from the special coordinate onward, padded by false elsewhere.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yGeSpecial n ω i = if ω.T ≤ i then CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yBit n ω i else false

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coarseConditioning (n : ℕ+) (ω : HardSample n) : Fin ↑n × (Fin ↑n → Bool) × (Fin ↑n → Bool)

The common coarse variable T, X_<T, Y_>T used in Claim 6.21.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceClaimConditioning (n : ℕ+) (ω : HardSample n) : Fin ↑n × (Fin ↑n → Bool) × (Fin ↑n → Bool)

The corrected Alice conditioning variable from (6.6): T, X_<T, Y_≥T.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceDynamicConditioning (n : ℕ+) (ω : HardSample n) : (Fin ↑n → Bool) × (Fin ↑n → Bool)

Alice's corrected conditioning data without the special coordinate: X_<T, Y_≥T.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceClaimConditioning_eq_specialCoordinate_prod_dynamic (n : ℕ+) : aliceClaimConditioning n = fun (ω : HardSample n) => (specialCoordinate n ω, aliceDynamicConditioning n ω)

Alice's corrected conditioning is the special coordinate together with the remaining conditioning data.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.bobClaimConditioning (n : ℕ+) (ω : HardSample n) : Fin ↑n × (Fin ↑n → Bool) × (Fin ↑n → Bool)

The corrected Bob conditioning variable from (6.6): T, X_≤T, Y_>T.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedXBit (n : ℕ+) (i : Fin ↑n) (ω : HardSample n) : Bool

Alice's fixed-coordinate bit used in Lemma 6.20.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedXBit n i ω = CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBit n ω i

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedXStrictPrefix (n : ℕ+) (i : Fin ↑n) (ω : HardSample n) : Fin ↑i → Bool

Alice's fixed-coordinate strict prefix X_<i, represented without padding.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedXStrictPrefix n i ω j = CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBit n ω ⟨↑j, ⋯⟩

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedXBefore (n : ℕ+) (i : Fin ↑n) (ω : HardSample n) : Fin ↑n → Bool

Alice's fixed-coordinate X_<i prefix used in Lemma 6.20.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedXBefore n i ω j = if j < i then CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBit n ω j else false

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedYBefore (n : ℕ+) (i : Fin ↑n) (ω : HardSample n) : Fin ↑n → Bool

Bob's fixed-coordinate Y_<i prefix used in Lemma 6.20.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedYBefore n i ω j = if j < i then CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yBit n ω j else false

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedYGe (n : ℕ+) (i : Fin ↑n) (ω : HardSample n) : Fin ↑n → Bool

Bob's fixed-coordinate Y_≥i suffix used in Lemma 6.20.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedYGe n i ω j = if i ≤ j then CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yBit n ω j else false

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedAliceConditioning (n : ℕ+) (i : Fin ↑n) (ω : HardSample n) : (Fin ↑n → Bool) × (Fin ↑n → Bool)

The fixed-coordinate Alice conditioning variable X_<i, Y_≥i from Lemma 6.20.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedAliceFullYConditioning (n : ℕ+) (i : Fin ↑n) (ω : HardSample n) : (Fin ↑i → Bool) × (Fin ↑n → Bool)

The fixed-coordinate conditioning variable (X_<i, Y) used in the chain-rule sum in Lemma 6.20. The X_<i prefix is represented without padding so that recodings are injective.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedAliceChainConditioningValue (n : ℕ+) (i : Fin ↑n) (c : (Fin ↑i → Bool) × (Fin ↑n → Bool)) : (Fin ↑n → Bool) × (Fin ↑n → Bool) × (Fin ↑n → Bool)

Recode (X_<i, Y) as (Y_<i, X_<i, Y_≥i), the conditioning variable produced by the textbook chain-rule split.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedAliceChainConditioningValue_injective (n : ℕ+) (i : Fin ↑n) : Function.Injective (fixedAliceChainConditioningValue n i)

The chain-rule conditioning (Y_<i, X_<i, Y_≥i) is an injective recoding of (X_<i, Y).

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedAliceChainConditioningValue_fixedAliceFullYConditioning (n : ℕ+) (i : Fin ↑n) : fixedAliceChainConditioningValue n i ∘ fixedAliceFullYConditioning n i = fun (ω : HardSample n) => (fixedYBefore n i ω, fixedAliceConditioning n i ω)

On hard samples, recoding (X_<i, Y) gives exactly (Y_<i, X_<i, Y_≥i).

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceClaimConditioningYFalseValues (n : ℕ+) : Set (Fin ↑n × (Fin ↑n → Bool) × (Fin ↑n → Bool))

The values of Alice's corrected conditioning variable for which Y_T = false.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceClaimConditioningYFalseValues n = {c : Fin ↑n × (Fin ↑n → Bool) × (Fin ↑n → Bool) | c.2.2 c.1 = false}

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yGeSpecial_specialCoordinate (n : ℕ+) (ω : HardSample n) : yGeSpecial n ω (specialCoordinate n ω) = specialY n ω

The Y_≥T component of Alice's corrected conditioning contains the bit Y_T.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialY_false_eq_preimage_aliceClaimConditioningYFalseValues (n : ℕ+) : specialY n ⁻¹' {false} = aliceClaimConditioning n ⁻¹' aliceClaimConditioningYFalseValues n

The event Y_T=false is determined by Alice's corrected conditioning variable.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.dualConditioningValue (n : ℕ+) (c : Fin ↑n × (Fin ↑n → Bool) × (Fin ↑n → Bool)) : Fin ↑n × (Fin ↑n → Bool) × (Fin ↑n → Bool)

The conditioning-value recoding induced by reversing coordinates and swapping Alice/Bob.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.dualConditioningValue_dualConditioningValue (n : ℕ+) (c : Fin ↑n × (Fin ↑n → Bool) × (Fin ↑n → Bool)) : dualConditioningValue n (dualConditioningValue n c) = c

Recoding a conditioning value twice recovers the original value.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.dualConditioningValue_injective (n : ℕ+) : Function.Injective (dualConditioningValue n)

The conditioning-value duality map is injective.

@[reducible, inline]

abbrev CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ProtocolType (n : ℕ+) : Type

The deterministic protocol type for disjointness inputs of length n.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ProtocolType n = CommunicationComplexity.Deterministic.Protocol (Set (Fin ↑n)) (Set (Fin ↑n)) Bool

@[reducible, inline]

abbrev CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.TranscriptType (n : ℕ+) (p : ProtocolType n) : Type

The syntactic transcript type for a disjointness protocol.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.TranscriptType n p = CommunicationComplexity.Deterministic.Protocol.Transcript p

structure CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.RawZType (n : ℕ+) (p : ProtocolType n) : Type

The raw type of values of the Z = (M, T, X_<T, Y_>T) variable for a protocol.

• transcript : TranscriptType n p
• specialCoordinate : Fin ↑n
• xBefore : Fin ↑n → Bool
• yAfter : Fin ↑n → Bool

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.RawZType.ext (n : ℕ+) {p : ProtocolType n} {z z' : RawZType n p} (htranscript : z.transcript = z'.transcript) (hT : z.specialCoordinate = z'.specialCoordinate) (hxBefore : z.xBefore = z'.xBefore) (hyAfter : z.yAfter = z'.yAfter) : z = z'

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.RawZType.ext_iff {n : ℕ+} {p : ProtocolType n} {z z' : RawZType n p} : z = z' ↔ z.transcript = z'.transcript ∧ z.specialCoordinate = z'.specialCoordinate ∧ z.xBefore = z'.xBefore ∧ z.yAfter = z'.yAfter

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.RawZType.equivProd (n : ℕ+) (p : ProtocolType n) : RawZType n p ≃ TranscriptType n p × Fin ↑n × (Fin ↑n → Bool) × (Fin ↑n → Bool)

A raw Z value is equivalent to the product of its named fields.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.rawZTypeFintype (n : ℕ+) (p : ProtocolType n) : Fintype (RawZType n p)

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.rawZTypeDecidableEq (n : ℕ+) (p : ProtocolType n) : DecidableEq (RawZType n p)

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.rawZTypeDecidableEq n p = Classical.decEq (CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.RawZType n p)

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.rawZVariable (n : ℕ+) (p : ProtocolType n) (ω : HardSample n) : RawZType n p

The raw Z = (M, T, X_<T, Y_>T) variable used in Claim 6.21.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ZType (n : ℕ+) (p : ProtocolType n) : Type

The type of achievable values of the Z = (M, T, X_<T, Y_>T) variable for a protocol.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ZType.transcript (n : ℕ+) {p : ProtocolType n} (z : ZType n p) : TranscriptType n p

The transcript component of an achievable Z value.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ZType.transcript n z = (↑z).transcript

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ZType.specialCoordinate (n : ℕ+) {p : ProtocolType n} (z : ZType n p) : Fin ↑n

The special-coordinate component of an achievable Z value.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ZType.specialCoordinate n z = (↑z).specialCoordinate

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ZType.xBefore (n : ℕ+) {p : ProtocolType n} (z : ZType n p) : Fin ↑n → Bool

The X_<T component of an achievable Z value.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ZType.xBefore n z = (↑z).xBefore

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ZType.yAfter (n : ℕ+) {p : ProtocolType n} (z : ZType n p) : Fin ↑n → Bool

The Y_>T component of an achievable Z value.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ZType.yAfter n z = (↑z).yAfter

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ZType.raw (n : ℕ+) {p : ProtocolType n} (z : ZType n p) : RawZType n p

The raw value underlying an achievable Z value.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ZType.raw n z = ↑z

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ZType.achievable (n : ℕ+) {p : ProtocolType n} (z : ZType n p) : ∃ (ω : HardSample n), rawZVariable n p ω = raw n z

The achievability proof carried by a ZType value.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ZType.ext (n : ℕ+) {p : ProtocolType n} {z z' : ZType n p} (htranscript : transcript n z = transcript n z') (hT : specialCoordinate n z = specialCoordinate n z') (hxBefore : xBefore n z = xBefore n z') (hyAfter : yAfter n z = yAfter n z') : z = z'

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ZType.ext_iff {n : ℕ+} {p : ProtocolType n} {z z' : ZType n p} : z = z' ↔ transcript n z = transcript n z' ∧ specialCoordinate n z = specialCoordinate n z' ∧ xBefore n z = xBefore n z' ∧ yAfter n z = yAfter n z'

noncomputable instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zTypeFintype (n : ℕ+) (p : ProtocolType n) : Fintype (ZType n p)

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zTypeFintype n p = id inferInstance

instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zTypeMeasurableSpace (n : ℕ+) (p : ProtocolType n) : MeasurableSpace (ZType n p)

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zTypeMeasurableSpace n p = ⊤

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zVariable (n : ℕ+) (p : ProtocolType n) (ω : HardSample n) : ZType n p

The Z = (M, T, X_<T, Y_>T) variable used in Claim 6.21.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zVariable n p ω = ⟨CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.rawZVariable n p ω, ⋯⟩

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zFiber (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : Set (HardSample n)

The fiber of the Z = (M, T, X_<T, Y_>T) variable above a value z.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zFiber n p z = CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zVariable n p ⁻¹' {z}

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zOutput (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : Bool

The protocol output determined by a Z value, through its transcript leaf.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.run_eq_zOutput_of_zVariable_eq (n : ℕ+) (p : ProtocolType n) {z : ZType n p} {ω : HardSample n} (hω : zVariable n p ω = z) : Deterministic.Protocol.run p (X n ω) (Y n ω) = zOutput n p z

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.volume_zFiber_ne_zero (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : MeasureTheory.volume (zFiber n p z) ≠ 0

Every achievable Z fiber has positive ambient hard-distribution mass.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.inputProbabilityMeasure (n : ℕ+) : MeasureTheory.ProbabilityMeasure (Set (Fin ↑n) × Set (Fin ↑n))

The hard input distribution, as a probability measure on input pairs.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.inputProbabilityMeasure n = MeasureTheory.ProbabilityMeasure.map ⟨MeasureTheory.volume, ⋯⟩ ⋯

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.inputDist (n : ℕ+) : FiniteProbabilitySpace (Set (Fin ↑n) × Set (Fin ↑n))

The hard input distribution packaged as a finite probability space for distributional error.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.dualProtocol (n : ℕ+) (p : ProtocolType n) : ProtocolType n

The protocol dual swaps Alice/Bob and reverses both coordinate sets.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.dualProtocolTranscriptMap (n : ℕ+) (p : ProtocolType n) : TranscriptType n p → TranscriptType n (dualProtocol n p)

The transcript-level map induced by protocol duality.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.dualProtocolTranscriptMap_injective (n : ℕ+) (p : ProtocolType n) : Function.Injective (dualProtocolTranscriptMap n p)

The transcript-level map induced by protocol duality is injective.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBit_of_ne_special (n : ℕ+) (ω : HardSample n) {i : Fin ↑n} (hi : i ≠ ω.T) : xBit n ω i = (ω.other i).xBit

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yBit_of_ne_special (n : ℕ+) (ω : HardSample n) {i : Fin ↑n} (hi : i ≠ ω.T) : yBit n ω i = (ω.other i).yBit

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.not_xBit_and_yBit_of_ne_special (n : ℕ+) (ω : HardSample n) {i : Fin ↑n} (hi : i ≠ ω.T) : ¬(xBit n ω i = true ∧ yBit n ω i = true)

Away from T, generated coordinate-pairs are disjoint.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateOfBits (x y : Bool) : DisjointCoordinate

The disjoint coordinate with the given bits. On the invalid (true, true) input this chooses an arbitrary disjoint coordinate; the projection lemmas below assume that invalid case away.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateOfBits_xBit {x y : Bool} (h : ¬(x = true ∧ y = true)) : (coordinateOfBits x y).xBit = x

coordinateOfBits preserves Alice's bit when the requested pair is disjoint.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateOfBits_yBit {x y : Bool} (h : ¬(x = true ∧ y = true)) : (coordinateOfBits x y).yBit = y

coordinateOfBits preserves Bob's bit when the requested pair is disjoint.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateOfBits_xBit_yBit (c : DisjointCoordinate) : coordinateOfBits c.xBit c.yBit = c

coordinateOfBits reconstructs an existing disjoint coordinate from its two projections.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.mix (n : ℕ+) (ωX ωY : HardSample n) : HardSample n

Mix Alice's input from ωX with Bob's input from ωY. This is only intended to be used when the two samples agree on T, X_<T, and Y_>T; under those hypotheses the mixed coordinate requests are always disjoint.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjoint_X_Y_iff (n : ℕ+) (ω : HardSample n) : Disjoint (X n ω) (Y n ω) ↔ ¬(ω.xT = true ∧ ω.yT = true)

The generated sets are disjoint exactly when the two special-coordinate bits are not both true.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCoordinateVector (n : ℕ+) (ω : HardSample n) : Fin ↑n → DisjointCoordinate

The generated disjoint coordinate-pair vector. On samples outside D, the special coordinate uses the arbitrary default built into coordinateOfBits.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCoordinateVector_xBit_of_mem_disjointEvent (n : ℕ+) {ω : HardSample n} (hω : ω ∈ disjointEvent n) (i : Fin ↑n) : (disjointCoordinateVector n ω i).xBit = xBit n ω i

On disjoint samples, the generated coordinate vector recovers Alice's input bit at every coordinate.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCoordinateVector_yBit_of_mem_disjointEvent (n : ℕ+) {ω : HardSample n} (hω : ω ∈ disjointEvent n) (i : Fin ↑n) : (disjointCoordinateVector n ω i).yBit = yBit n ω i

On disjoint samples, the generated coordinate vector recovers Bob's input bit at every coordinate.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ignoredCoordinate (n : ℕ+) (ω : HardSample n) : DisjointCoordinate

The other value at the special coordinate is ignored by the generated input.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.ignoredCoordinate n ω = ω.other ω.T

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointModel (n : ℕ+) (ω : HardSample n) : Fin ↑n × (Fin ↑n → DisjointCoordinate) × DisjointCoordinate

Coordinates for the conditioned-on-disjointness sample space: the special coordinate, the generated disjoint coordinate-pair vector, and the ignored other value at the special coordinate.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointEventFintype (n : ℕ+) : Fintype { ω : HardSample n // ω ∈ disjointEvent n }

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointEventInterDisjointModelFintype (n : ℕ+) (z : Fin ↑n × (Fin ↑n → DisjointCoordinate) × DisjointCoordinate) : Fintype { ω : HardSample n // ω ∈ disjointEvent n ∩ disjointModel n ⁻¹' {z} }

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.card_disjointEvent_inter_disjointModel_fiber (n : ℕ+) (z : Fin ↑n × (Fin ↑n → DisjointCoordinate) × DisjointCoordinate) : Fintype.card { ω : HardSample n // ω ∈ disjointEvent n ∩ disjointModel n ⁻¹' {z} } = 1

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.measureReal_disjointEvent_inter_disjointModel_fiber (n : ℕ+) (z : Fin ↑n × (Fin ↑n → DisjointCoordinate) × DisjointCoordinate) : MeasureTheory.volume.real (disjointEvent n ∩ disjointModel n ⁻¹' {z}) = 1 / (↑↑n * 4 * 3 ^ ↑n)

Under the hard distribution, a singleton fiber of the disjoint model together with D has one ambient sample's worth of mass.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.dualHardSample (n : ℕ+) (ω : HardSample n) : HardSample n

Dualize the hard sample space by swapping Alice/Bob and reversing coordinate order.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.dualHardSample n ω = { T := ω.T.rev, xT := ω.yT, yT := ω.xT, other := fun (i : Fin ↑n) => (ω.other i.rev).swap }

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.dualHardSample_dualHardSample (n : ℕ+) (ω : HardSample n) : dualHardSample n (dualHardSample n ω) = ω

Dualizing a hard sample twice recovers the original sample.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBit_dualHardSample (n : ℕ+) (ω : HardSample n) (i : Fin ↑n) : xBit n (dualHardSample n ω) i = yBit n ω i.rev

Alice's bit in the dual hard sample is Bob's original bit at the reversed coordinate.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yBit_dualHardSample (n : ℕ+) (ω : HardSample n) (i : Fin ↑n) : yBit n (dualHardSample n ω) i = xBit n ω i.rev

Bob's bit in the dual hard sample is Alice's original bit at the reversed coordinate.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.X_dualHardSample (n : ℕ+) (ω : HardSample n) : X n (dualHardSample n ω) = reverseSet n (Y n ω)

Dual hard samples swap Alice's input with Bob's input and reverse coordinates.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.Y_dualHardSample (n : ℕ+) (ω : HardSample n) : Y n (dualHardSample n ω) = reverseSet n (X n ω)

Dual hard samples swap Bob's input with Alice's input and reverse coordinates.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.input_dualHardSample (n : ℕ+) (ω : HardSample n) : input n (dualHardSample n ω) = (reverseSet n (Y n ω), reverseSet n (X n ω))

The generated input of a dual hard sample is the reversed, swapped original input.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointEvent_dualHardSample (n : ℕ+) (ω : HardSample n) : dualHardSample n ω ∈ disjointEvent n ↔ ω ∈ disjointEvent n

Hard-sample duality preserves the disjoint-input event.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialX_dualHardSample (n : ℕ+) (ω : HardSample n) : specialX n (dualHardSample n ω) = specialY n ω

Alice's special bit in the dual hard sample is Bob's original special bit.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialY_dualHardSample (n : ℕ+) (ω : HardSample n) : specialY n (dualHardSample n ω) = specialX n ω

Bob's special bit in the dual hard sample is Alice's original special bit.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialZeroZero_dualHardSample (n : ℕ+) (ω : HardSample n) : dualHardSample n ω ∈ specialZeroZero n ↔ ω ∈ specialZeroZero n

The X_T=Y_T=false slice is invariant under hard-sample duality.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xVector_dualHardSample (n : ℕ+) (ω : HardSample n) : xVector n (dualHardSample n ω) = reverseBoolVector n (yVector n ω)

Alice's full input vector in the dual is Bob's original full vector in reverse order.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yVector_dualHardSample (n : ℕ+) (ω : HardSample n) : yVector n (dualHardSample n ω) = reverseBoolVector n (xVector n ω)

Bob's full input vector in the dual is Alice's original full vector in reverse order.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBeforeSpecial_dualHardSample (n : ℕ+) (ω : HardSample n) : xBeforeSpecial n (dualHardSample n ω) = reverseBoolVector n (yAfterSpecial n ω)

Alice's before-special vector in the dual is Bob's after-special vector in reverse order.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yAfterSpecial_dualHardSample (n : ℕ+) (ω : HardSample n) : yAfterSpecial n (dualHardSample n ω) = reverseBoolVector n (xBeforeSpecial n ω)

Bob's after-special vector in the dual is Alice's before-special vector in reverse order.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xLeSpecial_dualHardSample (n : ℕ+) (ω : HardSample n) : xLeSpecial n (dualHardSample n ω) = reverseBoolVector n (yGeSpecial n ω)

Alice's X_≤T vector in the dual is Bob's Y_≥T vector in reverse order.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yGeSpecial_dualHardSample (n : ℕ+) (ω : HardSample n) : yGeSpecial n (dualHardSample n ω) = reverseBoolVector n (xLeSpecial n ω)

Bob's Y_≥T vector in the dual is Alice's X_≤T vector in reverse order.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coarseConditioning_dualHardSample (n : ℕ+) (ω : HardSample n) : coarseConditioning n (dualHardSample n ω) = dualConditioningValue n (coarseConditioning n ω)

The coarse Z conditioning data is self-dual up to the conditioning-value recoding.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceClaimConditioning_dualHardSample (n : ℕ+) (ω : HardSample n) : aliceClaimConditioning n (dualHardSample n ω) = dualConditioningValue n (bobClaimConditioning n ω)

Alice's corrected conditioning in the dual is Bob's corrected conditioning in recoded form.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.bobClaimConditioning_dualHardSample (n : ℕ+) (ω : HardSample n) : bobClaimConditioning n (dualHardSample n ω) = dualConditioningValue n (aliceClaimConditioning n ω)

Bob's corrected conditioning in the dual is Alice's corrected conditioning in recoded form.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.not_xBit_left_and_yBit_right_of_same_conditioning (n : ℕ+) {ωX ωY : HardSample n} (hT : ωX.T = ωY.T) (hBefore : xBeforeSpecial n ωX = xBeforeSpecial n ωY) (hAfter : yAfterSpecial n ωX = yAfterSpecial n ωY) {i : Fin ↑n} (hi : i ≠ ωX.T) : ¬(xBit n ωX i = true ∧ yBit n ωY i = true)

If two samples agree on the data contained in Z, then Alice's bit from the first sample and Bob's bit from the second sample are disjoint away from the special coordinate.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBit_mix (n : ℕ+) {ωX ωY : HardSample n} (hT : ωX.T = ωY.T) (hBefore : xBeforeSpecial n ωX = xBeforeSpecial n ωY) (hAfter : yAfterSpecial n ωX = yAfterSpecial n ωY) (i : Fin ↑n) : xBit n (mix n ωX ωY) i = xBit n ωX i

The mixed sample has Alice's input bits from the first sample.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yBit_mix (n : ℕ+) {ωX ωY : HardSample n} (hT : ωX.T = ωY.T) (hBefore : xBeforeSpecial n ωX = xBeforeSpecial n ωY) (hAfter : yAfterSpecial n ωX = yAfterSpecial n ωY) (i : Fin ↑n) : yBit n (mix n ωX ωY) i = yBit n ωY i

The mixed sample has Bob's input bits from the second sample.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.X_mix (n : ℕ+) {ωX ωY : HardSample n} (hT : ωX.T = ωY.T) (hBefore : xBeforeSpecial n ωX = xBeforeSpecial n ωY) (hAfter : yAfterSpecial n ωX = yAfterSpecial n ωY) : X n (mix n ωX ωY) = X n ωX

The mixed sample has Alice's full input from the first sample.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.Y_mix (n : ℕ+) {ωX ωY : HardSample n} (hT : ωX.T = ωY.T) (hBefore : xBeforeSpecial n ωX = xBeforeSpecial n ωY) (hAfter : yAfterSpecial n ωX = yAfterSpecial n ωY) : Y n (mix n ωX ωY) = Y n ωY

The mixed sample has Bob's full input from the second sample.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.input_mix (n : ℕ+) {ωX ωY : HardSample n} (hT : ωX.T = ωY.T) (hBefore : xBeforeSpecial n ωX = xBeforeSpecial n ωY) (hAfter : yAfterSpecial n ωX = yAfterSpecial n ωY) : input n (mix n ωX ωY) = (X n ωX, Y n ωY)

The mixed sample's generated input is the mixed input pair.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBeforeSpecial_mix (n : ℕ+) {ωX ωY : HardSample n} (hT : ωX.T = ωY.T) (hBefore : xBeforeSpecial n ωX = xBeforeSpecial n ωY) (hAfter : yAfterSpecial n ωX = yAfterSpecial n ωY) : xBeforeSpecial n (mix n ωX ωY) = xBeforeSpecial n ωX

Mixing preserves Alice's before-T conditioning data from the first sample.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yAfterSpecial_mix (n : ℕ+) {ωX ωY : HardSample n} (hT : ωX.T = ωY.T) (hBefore : xBeforeSpecial n ωX = xBeforeSpecial n ωY) (hAfter : yAfterSpecial n ωX = yAfterSpecial n ωY) : yAfterSpecial n (mix n ωX ωY) = yAfterSpecial n ωY

Mixing preserves Bob's after-T conditioning data from the second sample.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialX_mix (n : ℕ+) (ωX ωY : HardSample n) : specialX n (mix n ωX ωY) = specialX n ωX

The mixed sample has Alice's special bit from the first sample.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialY_mix (n : ℕ+) (ωX ωY : HardSample n) : specialY n (mix n ωX ωY) = specialY n ωY

The mixed sample has Bob's special bit from the second sample.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.mix_mix_swap (n : ℕ+) {ωX ωY : HardSample n} (hT : ωX.T = ωY.T) (hBefore : xBeforeSpecial n ωX = xBeforeSpecial n ωY) (hAfter : yAfterSpecial n ωX = yAfterSpecial n ωY) : mix n (mix n ωX ωY) (mix n ωY ωX) = ωX

Swapping twice recovers the first sample. This is the involution behind the rectangle-counting argument for conditional independence on Z fibers.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.hardSample_measureReal_fieldProduct (n : ℕ+) (TSet : Set (Fin ↑n)) (XSet YSet : Set Bool) (OtherSet : Set (Fin ↑n → DisjointCoordinate)) : MeasureTheory.volume.real {ω : HardSample n | ω.T ∈ TSet ∧ ω.xT ∈ XSet ∧ ω.yT ∈ YSet ∧ ω.other ∈ OtherSet} = (↑(uniformFin n)).real TSet * (↑uniformBool).real XSet * (↑uniformBool).real YSet * (↑(uniformDisjointCoordinateVector n)).real OtherSet

The hard sample distribution is the product distribution on the independent fields T, X_T, Y_T, and other. This rectangle form is the most convenient way to compute probabilities of events depending separately on the four fields.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.measureReal_specialIntersect (n : ℕ+) : MeasureTheory.volume.real (specialIntersect n) = 1 / 4

The hard distribution creates an intersection with probability 1 / 4.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.measureReal_specialBitsEvent (n : ℕ+) (bx bY : Bool) : MeasureTheory.volume.real (specialBitsEvent n bx bY) = 1 / 4

Each prescribed pair of special-coordinate bits has probability 1 / 4.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.measureReal_specialCoordinateEvent (n : ℕ+) (i : Fin ↑n) : MeasureTheory.volume.real (specialCoordinateEvent n i) = 1 / ↑↑n

Under the hard distribution, the special coordinate is uniform.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.measureReal_specialCoordinateEvent_inter_specialIntersect (n : ℕ+) (i : Fin ↑n) : MeasureTheory.volume.real (specialCoordinateEvent n i ∩ specialIntersect n) = 1 / (4 * ↑↑n)

Under the hard distribution, T=i and the special bits intersect with probability 1/(4n).

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.measureReal_specialZeroZero (n : ℕ+) : MeasureTheory.volume.real (specialZeroZero n) = 1 / 4

The event (X_T, Y_T) = (0, 0) has probability 1 / 4.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.measureReal_specialY_false (n : ℕ+) : MeasureTheory.volume.real (specialY n ⁻¹' {false}) = 1 / 2

The event Y_T = false has probability 1 / 2.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointEvent_eq_compl_specialIntersect (n : ℕ+) : disjointEvent n = (specialIntersect n)ᶜ

The disjoint event is the complement of the special-intersection event.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.measureReal_disjointEvent (n : ℕ+) : MeasureTheory.volume.real (disjointEvent n) = 3 / 4

The hard distribution generates disjoint inputs with probability 3 / 4.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.measureReal_specialCoordinateEvent_inter_disjointEvent (n : ℕ+) (i : Fin ↑n) : MeasureTheory.volume.real (specialCoordinateEvent n i ∩ disjointEvent n) = 3 / (4 * ↑↑n)

Under the hard distribution, T=i and disjointness have probability 3/(4n).

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.measure_disjointEvent_ne_zero (n : ℕ+) : MeasureTheory.volume (disjointEvent n) ≠ 0

The disjoint event has positive measure under the hard distribution.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCondMeasure (n : ℕ+) : MeasureTheory.Measure (HardSample n)

The hard distribution conditioned on the generated input being disjoint.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCondMeasure_measureReal_specialCoordinateEvent (n : ℕ+) (i : Fin ↑n) : (disjointCondMeasure n).real (specialCoordinateEvent n i) = 1 / ↑↑n

Under the disjoint-conditioned hard distribution, the special coordinate remains uniform.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialCoordinate_preimage_singleton (n : ℕ+) (i : Fin ↑n) : specialCoordinate n ⁻¹' {i} = specialCoordinateEvent n i

The special-coordinate singleton event is the corresponding named event.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCondMeasure_measureReal_specialCoordinate_preimage_singleton (n : ℕ+) (i : Fin ↑n) : (disjointCondMeasure n).real (specialCoordinate n ⁻¹' {i}) = 1 / ↑↑n

Under the disjoint-conditioned distribution, preimages of special-coordinate singletons have the uniform mass.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCondMeasure_ae_disjointEvent (n : ℕ+) : ∀ᵐ (ω : HardSample n) ∂disjointCondMeasure n, ω ∈ disjointEvent n

Under the measure conditioned on disjointness, the disjointness event holds almost surely.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.mem_disjointEvent_of_specialY_eq_false (n : ℕ+) {ω : HardSample n} (hY : specialY n ω = false) : ω ∈ disjointEvent n

If Bob's special bit is false, the generated inputs are disjoint.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialBitsEvent_subset_disjointEvent (n : ℕ+) (bx bY : Bool) (hbits : ¬(bx = true ∧ bY = true)) : specialBitsEvent n bx bY ⊆ disjointEvent n

A prescribed special-coordinate bit pair is disjoint exactly when it is not (true,true).

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialZeroZero_subset_disjointEvent (n : ℕ+) : specialZeroZero n ⊆ disjointEvent n

The (X_T,Y_T)=(0,0) slice is contained in the disjoint event.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCondMeasure_measureReal_specialZeroZero (n : ℕ+) : (disjointCondMeasure n).real (specialZeroZero n) = 1 / 3

Under the disjoint-conditioned hard distribution, (X_T,Y_T)=(0,0) has mass 1 / 3.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCondMeasure_measureReal_specialBitsEvent (n : ℕ+) (bx bY : Bool) (hbits : ¬(bx = true ∧ bY = true)) : (disjointCondMeasure n).real (specialBitsEvent n bx bY) = 1 / 3

Under the disjoint-conditioned hard distribution, each non-intersecting special bit-pair has mass 1/3.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCondMeasure_measureReal_specialY_false (n : ℕ+) : (disjointCondMeasure n).real (specialY n ⁻¹' {false}) = 2 / 3

Under the disjoint-conditioned hard distribution, Y_T=false has mass 2 / 3.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointSpecialYFalseMeasure (n : ℕ+) : MeasureTheory.Measure (HardSample n)

The disjoint-conditioned hard distribution, further conditioned on Bob's special bit being false. This is the Alice-side conditioning used in the Claim 6.21 Pinsker step.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointSpecialYFalseMeasure_isProbabilityMeasure (n : ℕ+) : MeasureTheory.IsProbabilityMeasure (disjointSpecialYFalseMeasure n)

Conditioning the disjoint law on Y_T = false gives a probability measure.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointSpecialYFalseMeasure_measureReal_specialX_singleton (n : ℕ+) (b : Bool) : (disjointSpecialYFalseMeasure n).real (specialX n ⁻¹' {b}) = 1 / 2

Under D ∧ Y_T=false, Alice's special bit is uniform.

instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCondMeasure_isProbabilityMeasure (n : ℕ+) : MeasureTheory.IsProbabilityMeasure (disjointCondMeasure n)

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCondMeasure_measureReal_disjointModel_fiber (n : ℕ+) (z : Fin ↑n × (Fin ↑n → DisjointCoordinate) × DisjointCoordinate) : (disjointCondMeasure n).real (disjointModel n ⁻¹' {z}) = 1 / (↑↑n * 3 ^ ↑n * 3)

Under the disjoint-conditioned distribution, the disjoint model is uniform.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.card_disjointModel_fiber_for_coordinateVector (n : ℕ+) (coords : Fin ↑n → DisjointCoordinate) : Fintype.card { z : Fin ↑n × (Fin ↑n → DisjointCoordinate) × DisjointCoordinate // z.2.1 = coords } = ↑n * 3

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.card_disjointModel_fiber_for_specialCoordinate_coordinateVector (n : ℕ+) (i : Fin ↑n) (coords : Fin ↑n → DisjointCoordinate) : Fintype.card { z : Fin ↑n × (Fin ↑n → DisjointCoordinate) × DisjointCoordinate // z.1 = i ∧ z.2.1 = coords } = 3

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCondMeasure_measureReal_disjointCoordinateVector_fiber (n : ℕ+) (coords : Fin ↑n → DisjointCoordinate) : (disjointCondMeasure n).real (disjointCoordinateVector n ⁻¹' {coords}) = 1 / 3 ^ ↑n

Under the disjoint-conditioned distribution, the generated disjoint coordinate vector is uniform over the 3^n disjoint coordinate vectors.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCondMeasure_cond_specialCoordinate_measureReal_disjointCoordinateVector_fiber (n : ℕ+) (i : Fin ↑n) (coords : Fin ↑n → DisjointCoordinate) : (disjointCondMeasure n)[|specialCoordinate n ⁻¹' {i}].real (disjointCoordinateVector n ⁻¹' {coords}) = 1 / 3 ^ ↑n

Under D and T=i, the generated disjoint coordinate vector is still uniform over the 3^n disjoint coordinate vectors.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformDisjointCoordinateVector_eq_pi (n : ℕ+) : ↑(uniformDisjointCoordinateVector n) = MeasureTheory.Measure.pi fun (x : Fin ↑n) => ↑uniformDisjointCoordinate

The uniform law on disjoint coordinate vectors is the product of the one-coordinate uniform laws.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformDisjointCoordinateVector_iIndepFun (n : ℕ+) : ProbabilityTheory.iIndepFun (fun (i : Fin ↑n) (coords : Fin ↑n → DisjointCoordinate) => coords i) ↑(uniformDisjointCoordinateVector n)

Under the uniform disjoint-coordinate-vector law, the coordinates are independent.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateXBit (n : ℕ+) (i : Fin ↑n) (coords : Fin ↑n → DisjointCoordinate) : Bool

Alice's bit at a fixed coordinate of a generated disjoint coordinate vector.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateXBit n i coords = (coords i).xBit

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateYBit (n : ℕ+) (i : Fin ↑n) (coords : Fin ↑n → DisjointCoordinate) : Bool

Bob's bit at a fixed coordinate of a generated disjoint coordinate vector.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateYBit n i coords = (coords i).yBit

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateXSet (n : ℕ+) (coords : Fin ↑n → DisjointCoordinate) : Set (Fin ↑n)

Alice's input set represented by a generated disjoint coordinate vector.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateYSet (n : ℕ+) (coords : Fin ↑n → DisjointCoordinate) : Set (Fin ↑n)

Bob's input set represented by a generated disjoint coordinate vector.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateInput (n : ℕ+) (coords : Fin ↑n → DisjointCoordinate) : Set (Fin ↑n) × Set (Fin ↑n)

The input pair represented by a generated disjoint coordinate vector.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateMessage (n : ℕ+) (p : ProtocolType n) (coords : Fin ↑n → DisjointCoordinate) : TranscriptType n p

The protocol transcript as a function of the generated disjoint coordinate vector.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateXBefore (n : ℕ+) (i : Fin ↑n) (coords : Fin ↑n → DisjointCoordinate) : Fin ↑n → Bool

Alice's coordinate-vector bits before a fixed coordinate, padded by false elsewhere.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateYBefore (n : ℕ+) (i : Fin ↑n) (coords : Fin ↑n → DisjointCoordinate) : Fin ↑n → Bool

Bob's coordinate-vector bits before a fixed coordinate, padded by false elsewhere.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateYGe (n : ℕ+) (i : Fin ↑n) (coords : Fin ↑n → DisjointCoordinate) : Fin ↑n → Bool

Bob's coordinate-vector bits from a fixed coordinate onward, padded by false elsewhere.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateAliceConditioning (n : ℕ+) (i : Fin ↑n) (coords : Fin ↑n → DisjointCoordinate) : (Fin ↑n → Bool) × (Fin ↑n → Bool)

The coordinate-vector version of Alice's fixed-coordinate Lemma 6.20 conditioning.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateAliceCondBit (n : ℕ+) (i k : Fin ↑n) (coords : Fin ↑n → DisjointCoordinate) : Bool

The one-bit-per-coordinate version of Alice's fixed conditioning: use X_j before i and Y_j from i onward.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateAliceCondBits (n : ℕ+) (i : Fin ↑n) (coords : Fin ↑n → DisjointCoordinate) : Fin ↑n → Bool

Alice's fixed conditioning as one bit from each coordinate.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateAliceResidualBit (n : ℕ+) (i k : Fin ↑n) (coords : Fin ↑n → DisjointCoordinate) : Bool

The residual coordinate bit left after conditioning on coordinateAliceCondBit. Before i this is Bob's bit; at i it is Alice's bit; after i it is unused.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateAliceConditioningOfCondBits (n : ℕ+) (i : Fin ↑n) (bits : Fin ↑n → Bool) : (Fin ↑n → Bool) × (Fin ↑n → Bool)

Recode the one-bit-per-coordinate Alice conditioning into the padded pair used in the information term.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateAliceConditioning_eq_recode_condBits (n : ℕ+) (i : Fin ↑n) : coordinateAliceConditioning n i = coordinateAliceConditioningOfCondBits n i ∘ coordinateAliceCondBits n i

The one-bit-per-coordinate conditioning recodes to the padded-pair conditioning.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateAliceConditioningOfCondBits_injective (n : ℕ+) (i : Fin ↑n) : Function.Injective (coordinateAliceConditioningOfCondBits n i)

The padded-pair recoding of Alice's one-bit-per-coordinate conditioning is injective.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateAliceCondBits_fiber_eq_iInter (n : ℕ+) (i : Fin ↑n) (bits : Fin ↑n → Bool) : coordinateAliceCondBits n i ⁻¹' {bits} = ⋂ (k : Fin ↑n), coordinateAliceCondBit n i k ⁻¹' {bits k}

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateWithCondBit (n : ℕ+) (i k : Fin ↑n) (b : Bool) : DisjointCoordinate

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coordinateWithCondBit_spec (n : ℕ+) (i k : Fin ↑n) (b : Bool) : (if k < i then (coordinateWithCondBit n i k b).xBit else (coordinateWithCondBit n i k b).yBit) = b

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformDisjointCoordinateVector_measure_condBit_ne_zero (n : ℕ+) (i k : Fin ↑n) (b : Bool) : ↑(uniformDisjointCoordinateVector n) (coordinateAliceCondBit n i k ⁻¹' {b}) ≠ 0

Each single-coordinate conditioning bit has positive mass under the uniform disjoint-vector law.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformDisjointCoordinateVector_residual_cond_iIndepFun (n : ℕ+) (i : Fin ↑n) : ProbabilityTheory.iIndepFun (fun (k : Fin ↑n) (coords : Fin ↑n → DisjointCoordinate) => (coordinateAliceResidualBit n i k coords, coordinateAliceCondBit n i k coords)) ↑(uniformDisjointCoordinateVector n)

The per-coordinate residual/conditioning pairs are independent under the product-uniform disjoint-coordinate law.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformDisjointCoordinateVector_indep_coordinateXBit_coordinateYBefore_condBits (n : ℕ+) (i : Fin ↑n) (bits : Fin ↑n → Bool) : ProbabilityTheory.IndepFun (coordinateXBit n i) (coordinateYBefore n i) (↑(uniformDisjointCoordinateVector n))[|coordinateAliceCondBits n i ⁻¹' {bits}]

After fixing Alice's one-bit-per-coordinate conditioning, the current Alice bit is independent of Bob's earlier bits under the product-uniform disjoint-coordinate law.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformDisjointCoordinateVector_crossInfo_condBits_eq_zero (n : ℕ+) (i : Fin ↑n) : I[coordinateXBit n i : coordinateYBefore n i|coordinateAliceCondBits n i;↑(uniformDisjointCoordinateVector n)] = 0

Product-coordinate form of the textbook independence input: I(X_i : Y_<i | X_<i,Y_≥i)=0, first with the one-bit-per-coordinate conditioning.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformDisjointCoordinateVector_crossInfo_eq_zero (n : ℕ+) (i : Fin ↑n) : I[coordinateXBit n i : coordinateYBefore n i|coordinateAliceConditioning n i;↑(uniformDisjointCoordinateVector n)] = 0

Product-coordinate form of the textbook independence input, using the padded-pair conditioning variable from Lemma 6.20.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedXBit_ae_eq_coordinateXBit (n : ℕ+) (i : Fin ↑n) : fixedXBit n i =ᵐ[disjointCondMeasure n] fun (ω : HardSample n) => coordinateXBit n i (disjointCoordinateVector n ω)

Under D, Alice's fixed bit is the corresponding coordinate-vector projection.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedYBefore_ae_eq_coordinateYBefore (n : ℕ+) (i : Fin ↑n) : fixedYBefore n i =ᵐ[disjointCondMeasure n] fun (ω : HardSample n) => coordinateYBefore n i (disjointCoordinateVector n ω)

Under D, Bob's fixed prefix is the corresponding coordinate-vector projection.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedAliceConditioning_ae_eq_coordinateAliceConditioning (n : ℕ+) (i : Fin ↑n) : fixedAliceConditioning n i =ᵐ[disjointCondMeasure n] fun (ω : HardSample n) => coordinateAliceConditioning n i (disjointCoordinateVector n ω)

Under D, Alice's fixed conditioning is the corresponding coordinate-vector projection.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.identDistrib_disjointCoordinateVector_uniform (n : ℕ+) : ProbabilityTheory.IdentDistrib (disjointCoordinateVector n) id (disjointCondMeasure n) ↑(uniformDisjointCoordinateVector n)

The generated disjoint coordinate vector under D has the uniform disjoint-vector law.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.identDistrib_disjointCoordinateVector_uniform_cond_specialCoordinate (n : ℕ+) (i : Fin ↑n) : ProbabilityTheory.IdentDistrib (disjointCoordinateVector n) id (disjointCondMeasure n)[|specialCoordinate n ⁻¹' {i}] ↑(uniformDisjointCoordinateVector n)

Even after conditioning on T=i, the generated disjoint coordinate vector has the uniform disjoint-vector law.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.identDistrib_self_comp_measurePreserving {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {T : Ω → Ω} (hT : MeasureTheory.MeasurePreserving T μ μ) (F : Ω → α) (hF : Measurable F) : ProbabilityTheory.IdentDistrib F (F ∘ T) μ μ

A measure-preserving self-map leaves every random variable identically distributed with its pullback along that map.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.dualHardSample_preimage_singleton (n : ℕ+) (ω : HardSample n) : dualHardSample n ⁻¹' {ω} = {dualHardSample n ω}

The preimage of a singleton under hard-sample duality is the dual singleton.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.volume_measureReal_singleton_dualHardSample (n : ℕ+) (ω : HardSample n) : MeasureTheory.volume.real {dualHardSample n ω} = MeasureTheory.volume.real {ω}

The uniform hard-sample measure gives the same mass to a sample and its dual.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.volume_measurePreserving_dualHardSample (n : ℕ+) : MeasureTheory.MeasurePreserving (dualHardSample n) MeasureTheory.volume MeasureTheory.volume

Hard-sample duality preserves the uniform hard-sample measure.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCondMeasure_measureReal_singleton_dualHardSample (n : ℕ+) (ω : HardSample n) : (disjointCondMeasure n).real {dualHardSample n ω} = (disjointCondMeasure n).real {ω}

The disjoint-conditioned hard-sample measure gives the same mass to a sample and its dual.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointCondMeasure_measurePreserving_dualHardSample (n : ℕ+) : MeasureTheory.MeasurePreserving (dualHardSample n) (disjointCondMeasure n) (disjointCondMeasure n)

Hard-sample duality preserves the disjoint-conditioned hard-sample measure.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.volume_cond_eq_disjointCondMeasure_cond_of_subset_disjointEvent (n : ℕ+) {A : Set (HardSample n)} (hA : A ⊆ disjointEvent n) : MeasureTheory.volume[|A] = (disjointCondMeasure n)[|A]

Conditioning on a subevent of disjointness is the same under the ambient hard distribution and under the hard distribution first conditioned on disjointness.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.volume_cond_specialZeroZero_measureReal_le_two_mul_disjointSpecialYFalseMeasure (n : ℕ+) (S : Set (HardSample n)) : MeasureTheory.volume[|specialZeroZero n].real S ≤ 2 * (disjointSpecialYFalseMeasure n).real S

Conditioning on (X_T,Y_T)=(0,0) costs at most a factor 2 relative to conditioning only on Y_T=false under the disjoint distribution. This is the reweighting step before Markov in Claim 6.21.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.message (n : ℕ+) (p : ProtocolType n) (ω : HardSample n) : TranscriptType n p

The transcript random variable induced by a deterministic protocol on the hard sample space.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.message_ae_eq_coordinateMessage (n : ℕ+) (p : ProtocolType n) : message n p =ᵐ[disjointCondMeasure n] fun (ω : HardSample n) => coordinateMessage n p (disjointCoordinateVector n ω)

Under D, the transcript is a function of the generated disjoint coordinate vector.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.entropy_message_le_complexity_mul_log_two_of_measure (n : ℕ+) (p : ProtocolType n) (μ : MeasureTheory.Measure (HardSample n)) : H[message n p; μ] ≤ ↑(Deterministic.Protocol.complexity p) * Real.log 2

The transcript entropy is at most the protocol length in bits, for any ambient measure.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.message_dualProtocol_dualHardSample (n : ℕ+) (p : ProtocolType n) (ω : HardSample n) : message n (dualProtocol n p) (dualHardSample n ω) = dualProtocolTranscriptMap n p (message n p ω)

The dual protocol transcript on the dual hard sample is the original transcript recoded through protocol duality.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.dualRawZValue (n : ℕ+) (p : ProtocolType n) (z : RawZType n p) : RawZType n (dualProtocol n p)

Dualize a raw Z = (M,T,X_<T,Y_>T) value by recoding the transcript and coarse conditioning data.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.rawZVariable_dualProtocol_dualHardSample (n : ℕ+) (p : ProtocolType n) (ω : HardSample n) : rawZVariable n (dualProtocol n p) (dualHardSample n ω) = dualRawZValue n p (rawZVariable n p ω)

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.dualZValue (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : ZType n (dualProtocol n p)

Dualize an achievable Z = (M,T,X_<T,Y_>T) value by recoding the transcript and coarse conditioning data.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.dualRawZValue_injective (n : ℕ+) (p : ProtocolType n) : Function.Injective (dualRawZValue n p)

Raw Z dualization is injective.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.dualZValue_injective (n : ℕ+) (p : ProtocolType n) : Function.Injective (dualZValue n p)

The Z-value recoding induced by protocol and hard-sample duality is injective.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zVariable_dualProtocol_dualHardSample (n : ℕ+) (p : ProtocolType n) (ω : HardSample n) : zVariable n (dualProtocol n p) (dualHardSample n ω) = dualZValue n p (zVariable n p ω)

The Z variable for the dual protocol and hard sample is the recoded original Z.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zVariable_dualProtocol_preimage_dualZValue (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : dualHardSample n ⁻¹' zFiber n (dualProtocol n p) (dualZValue n p z) = zFiber n p z

Pulling a recoded dual Z fiber back along hard-sample duality gives the original Z fiber.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.volume_zVariable_dualProtocol_dualZValue (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : MeasureTheory.volume (zFiber n (dualProtocol n p) (dualZValue n p z)) = MeasureTheory.volume (zFiber n p z)

The ambient hard-sample measure gives corresponding original and dual Z fibers the same mass.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.volume_measureReal_zVariable_dualProtocol_dualZValue (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : MeasureTheory.volume.real (zFiber n (dualProtocol n p) (dualZValue n p z)) = MeasureTheory.volume.real (zFiber n p z)

Real-valued version of volume_zVariable_dualProtocol_dualZValue.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.inputDist_measureReal_eq_preimage (n : ℕ+) (S : Set (Set (Fin ↑n) × Set (Fin ↑n))) : MeasureTheory.volume.real S = MeasureTheory.volume.real (input n ⁻¹' S)

Probabilities under the hard input distribution can be computed on the explicit hard sample space by taking preimages under input.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.protocolErrorEvent (n : ℕ+) (p : ProtocolType n) : Set (HardSample n)

The sample-space event where a deterministic protocol errs on disjointness.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.distributionalError_inputDist_eq_protocolErrorEvent (n : ℕ+) (p : ProtocolType n) : Deterministic.Protocol.distributionalError p (inputDist n) (disjointness ↑n) = MeasureTheory.volume.real (protocolErrorEvent n p)

Distributional error under the hard input distribution is the probability of the named sample-space error event.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialPair (n : ℕ+) (ω : HardSample n) : Bool × Bool

The special-coordinate bit-pair.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointSpecialYFalseMeasure_specialX_law_eq_uniformBool (n : ℕ+) : MeasureTheory.ProbabilityMeasure.map ⟨disjointSpecialYFalseMeasure n, ⋯⟩ ⋯ = uniformBool

The law of X_T under D ∧ Y_T=false is the uniform bit law.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformBool_toPMF_ne_zero (b : Bool) : (↑uniformBool).toPMF b ≠ 0

The uniform law on one bit has full support.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.toReal_klDiv_bool_uniform_eq_KLDiv (μ : MeasureTheory.ProbabilityMeasure Bool) : (InformationTheory.klDiv ↑μ ↑uniformBool).toReal = KL[id ; ↑μ # id ; ↑uniformBool]

On one-bit probability measures, Mathlib's klDiv to the uniform bit law agrees with the real-valued PFR KLDiv used by the entropy API.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.toReal_klDiv_map_bool_uniform_eq_KLDiv_of_measureReal_ne_zero {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (X : Ω → Bool) (S : Set Ω) (hX : Measurable X) (hS : μ.real S ≠ 0) : (InformationTheory.klDiv (MeasureTheory.Measure.map X μ[|S]) ↑uniformBool).toReal = KL[X ; μ[|S] # id ; ↑uniformBool]

Positive conditional fibers let the Mathlib one-bit KL be read as the PFR real-valued KLDiv of the corresponding random variable.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformBoolPair : MeasureTheory.ProbabilityMeasure (Bool × Bool)

Uniform law on a bit-pair.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformBoolPair_singleton (b : Bool × Bool) : (↑uniformBoolPair).real {b} = 1 / 4

Each bit-pair has mass 1 / 4 under the uniform law on two bits.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.uniformBoolPair_eq_prod : uniformBoolPair = TVDistance.probabilityMeasureProd uniformBool uniformBool

The uniform law on two bits is the product of the one-bit uniform laws.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zFiberMeasure (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : MeasureTheory.Measure (HardSample n)

The hard-distribution measure conditioned on a Z=z fiber.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zFiberMeasure n p z = MeasureTheory.volume[|CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zFiber n p z]

instance CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zFiberMeasure_isProbabilityMeasure (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : MeasureTheory.IsProbabilityMeasure (zFiberMeasure n p z)

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zFiberMeasure_real_apply (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (S : Set (HardSample n)) : (zFiberMeasure n p z).real S = (MeasureTheory.volume.real (zFiber n p z))⁻¹ * MeasureTheory.volume.real (zFiber n p z ∩ S)

Conditional probabilities under a Z=z fiber are computed by intersecting with the fiber and dividing by its mass.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointSpecialYFalseMeasure_measureReal_zVariable (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : (disjointSpecialYFalseMeasure n).real (zFiber n p z) = 3 / 2 * (disjointCondMeasure n).real (specialY n ⁻¹' {false} ∩ zFiber n p z)

The mass of a Z fiber under the Alice-side conditioned measure, with the 3/2 scaling from Pr_D[Y_T=false]=2/3 made explicit.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointSpecialYFalseMeasure_cond_zVariable_eq_cond_inter (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : (disjointSpecialYFalseMeasure n)[|zVariable n p ⁻¹' {z}] = (disjointCondMeasure n)[|specialY n ⁻¹' {false} ∩ zFiber n p z]

Conditioning first on Y_T=false under D, then on a Z value, is the same as conditioning under D on the intersection of those events.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zFiberMeasure_cond_specialY_eq_volume_cond_inter (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (b : Bool) : (zFiberMeasure n p z)[|specialY n ⁻¹' {b}] = MeasureTheory.volume[|zFiber n p z ∩ specialY n ⁻¹' {b}]

Conditioning a Z=z fiber further on a special Bob-bit value is the same as conditioning the ambient hard distribution on the intersection of those two fiber events.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zFiberMeasure_cond_specialYFalse_eq_disjointSpecialYFalseMeasure_cond_zVariable (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : (zFiberMeasure n p z)[|specialY n ⁻¹' {false}] = (disjointSpecialYFalseMeasure n)[|zVariable n p ⁻¹' {z}]

Conditioning a Z=z fiber further on Y_T=false agrees with conditioning the D ∧ Y_T=false measure on the same Z fiber.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zFiberMeasure_specialYFalse_ne_zero_of_disjointSpecialYFalseMeasure_ne_zero (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (hz : (disjointSpecialYFalseMeasure n).real (zFiber n p z) ≠ 0) : (zFiberMeasure n p z).real (specialY n ⁻¹' {false}) ≠ 0

A positive Z=z fiber under D ∧ Y_T=false makes the Y_T=false branch of the ambient Z=z fiber positive.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.conditionalSpecialPairLaw (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : MeasureTheory.ProbabilityMeasure (Bool × Bool)

The conditional law of the special bit-pair on a positive-mass Z=z fiber.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.conditionalSpecialPairLaw_singleton (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (b : Bool × Bool) : (↑(conditionalSpecialPairLaw n p z)).real {b} = (zFiberMeasure n p z).real (specialPair n ⁻¹' {b})

On a positive-mass Z=z fiber, the conditional specialPair singleton mass is the corresponding preimage probability under the fiber measure.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.conditionalSpecialXLaw (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : MeasureTheory.ProbabilityMeasure Bool

The conditional law of Alice's special bit on a positive-mass Z=z fiber.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.conditionalSpecialYLaw (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : MeasureTheory.ProbabilityMeasure Bool

The conditional law of Bob's special bit on a positive-mass Z=z fiber.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.conditionalSpecialXLaw_singleton (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (b : Bool) : (↑(conditionalSpecialXLaw n p z)).real {b} = (zFiberMeasure n p z).real (specialX n ⁻¹' {b})

On a positive-mass Z=z fiber, Alice's conditional special-bit singleton mass is the corresponding preimage probability under the fiber measure.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.conditionalSpecialYLaw_singleton (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (b : Bool) : (↑(conditionalSpecialYLaw n p z)).real {b} = (zFiberMeasure n p z).real (specialY n ⁻¹' {b})

On a positive-mass Z=z fiber, Bob's conditional special-bit singleton mass is the corresponding preimage probability under the fiber measure.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zDistance (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : ℝ

The TV distance between the conditional special-pair law on a Z=z fiber and the uniform bit-pair law.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xDistance (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : ℝ

The TV distance between Alice's conditional special-bit law and a uniform bit.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yDistance (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : ℝ

The TV distance between Bob's conditional special-bit law and a uniform bit.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xDistance_nonneg (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : 0 ≤ xDistance n p z

Alice's one-bit conditional TV distance is nonnegative.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.dualHardSample_preimage_zVariable_dualZValue_inter_specialX (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (b : Bool) : dualHardSample n ⁻¹' (zFiber n (dualProtocol n p) (dualZValue n p z) ∩ specialX n ⁻¹' {b}) = zFiber n p z ∩ specialY n ⁻¹' {b}

Pulling a dual Z fiber intersected with a dual Alice-special-bit event back along hard-sample duality gives the corresponding original Bob-special-bit event.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.volume_zVariable_dualProtocol_dualZValue_inter_specialX (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (b : Bool) : MeasureTheory.volume (zFiber n (dualProtocol n p) (dualZValue n p z) ∩ specialX n ⁻¹' {b}) = MeasureTheory.volume (zFiber n p z ∩ specialY n ⁻¹' {b})

The ambient hard-sample measure gives corresponding original and dual one-bit Z-fiber events the same mass.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.volume_measureReal_zVariable_dualProtocol_dualZValue_inter_specialX (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (b : Bool) : MeasureTheory.volume.real (zFiber n (dualProtocol n p) (dualZValue n p z) ∩ specialX n ⁻¹' {b}) = MeasureTheory.volume.real (zFiber n p z ∩ specialY n ⁻¹' {b})

Real-valued version of volume_zVariable_dualProtocol_dualZValue_inter_specialX.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.conditionalSpecialXLaw_dualProtocol_dualZValue (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : conditionalSpecialXLaw n (dualProtocol n p) (dualZValue n p z) = conditionalSpecialYLaw n p z

The Alice one-bit law on the dual protocol's recoded Z fiber is Bob's one-bit law on the original Z fiber.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xDistance_dualProtocol_dualZValue_eq_yDistance (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : xDistance n (dualProtocol n p) (dualZValue n p z) = yDistance n p z

The Alice one-bit distance for the dual protocol at the recoded Z value is the original Bob one-bit distance.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.volume_specialZeroZero_inter_xDistance_dualProtocol_eq_yDistance (n : ℕ+) (p : ProtocolType n) (γ : ℝ) : MeasureTheory.volume.real (specialZeroZero n ∩ {ω : HardSample n | γ < xDistance n (dualProtocol n p) (zVariable n (dualProtocol n p) ω)}) = MeasureTheory.volume.real (specialZeroZero n ∩ {ω : HardSample n | γ < yDistance n p (zVariable n p ω)})

The dual Alice bad event on the X_T=Y_T=false slice is the original Bob bad event.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.two_mul_xDistance_sq_le_toReal_klDiv_uniformBool (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : 2 * xDistance n p z ^ 2 ≤ (InformationTheory.klDiv ↑(conditionalSpecialXLaw n p z) ↑uniformBool).toReal

Pinsker for Alice's one-bit fiber distance against the uniform bit.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xFiberKL (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : ℝ

Alice's one-bit fiber KL cost on a Z=z fiber.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.two_mul_xDistance_sq_le_xFiberKL (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : 2 * xDistance n p z ^ 2 ≤ xFiberKL n p z

Pointwise Pinsker for Alice.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.two_mul_integral_xDistance_sq_le_integral_xFiberKL_disjointSpecialYFalse (n : ℕ+) (p : ProtocolType n) : 2 * ∫ (ω : HardSample n), xDistance n p (zVariable n p ω) ^ 2 ∂disjointSpecialYFalseMeasure n ≤ ∫ (ω : HardSample n), xFiberKL n p (zVariable n p ω) ∂disjointSpecialYFalseMeasure n

Integrated Alice Pinsker bound over the D ∧ Y_T=false conditioned measure.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointSpecialYFalseMeasure_integral_xDistance_le_of_integral_sq_le (n : ℕ+) (p : ProtocolType n) {γ : ℝ} (hsq : ∫ (ω : HardSample n), xDistance n p (zVariable n p ω) ^ 2 ∂disjointSpecialYFalseMeasure n ≤ γ ^ 4) : ∫ (ω : HardSample n), xDistance n p (zVariable n p ω) ∂disjointSpecialYFalseMeasure n ≤ γ ^ 2

Jensen's inequality converts a squared Alice-side average-distance estimate under D ∧ Y_T=false into the average-distance estimate used before Markov.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointSpecialYFalseMeasure_xDistance_bad_le_of_integral_le (n : ℕ+) (p : ProtocolType n) {γ : ℝ} (hγ : 0 < γ) (havg : ∫ (ω : HardSample n), xDistance n p (zVariable n p ω) ∂disjointSpecialYFalseMeasure n ≤ γ ^ 2) : (disjointSpecialYFalseMeasure n).real {ω : HardSample n | γ < xDistance n p (zVariable n p ω)} ≤ γ

Markov's inequality converts the textbook Alice-side average-distance estimate under D ∧ Y_T=false into a bad-Z probability bound.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.goodZ (n : ℕ+) (p : ProtocolType n) (γ : ℝ) (z : ZType n p) : Prop

A Z value is good when the conditional special-pair law on its achievable fiber is within 2γ of uniform.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.goodZ n p γ z = (CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zDistance n p z ≤ 2 * γ)

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.goodZEvent (n : ℕ+) (p : ProtocolType n) (γ : ℝ) : Set (HardSample n)

The good-fiber event 𝓖 in Claim 6.21, pulled back to the hard sample space through Z.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.input_mem_transcript (n : ℕ+) (p : ProtocolType n) (ω : HardSample n) : input n ω ∈ Deterministic.Protocol.Transcript.inputSet (message n p ω)

The generated input follows the transcript of any deterministic protocol.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.input_mem_transcript_of_zVariable_eq (n : ℕ+) (p : ProtocolType n) {z : ZType n p} {ω : HardSample n} (hω : zVariable n p ω = z) : input n ω ∈ Deterministic.Protocol.Transcript.inputSet (ZType.transcript n z)

If a sample has Z=z, its generated input follows the transcript component of z.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialCoordinate_eq_of_zVariable_eq (n : ℕ+) (p : ProtocolType n) {z : ZType n p} {ω : HardSample n} (hω : zVariable n p ω = z) : specialCoordinate n ω = ZType.specialCoordinate n z

Equal Z value fixes the special coordinate.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBeforeSpecial_eq_of_zVariable_eq (n : ℕ+) (p : ProtocolType n) {z : ZType n p} {ω : HardSample n} (hω : zVariable n p ω = z) : xBeforeSpecial n ω = ZType.xBefore n z

Equal Z value fixes Alice's bits before the special coordinate.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yAfterSpecial_eq_of_zVariable_eq (n : ℕ+) (p : ProtocolType n) {z : ZType n p} {ω : HardSample n} (hω : zVariable n p ω = z) : yAfterSpecial n ω = ZType.yAfter n z

Equal Z value fixes Bob's bits after the special coordinate.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.mixed_inputs_mem_transcript_of_zVariable_eq (n : ℕ+) (p : ProtocolType n) {z : ZType n p} {ω ω' : HardSample n} (hω : zVariable n p ω = z) (hω' : zVariable n p ω' = z) : (X n ω', Y n ω) ∈ Deterministic.Protocol.Transcript.inputSet (ZType.transcript n z) ∧ (X n ω, Y n ω') ∈ Deterministic.Protocol.Transcript.inputSet (ZType.transcript n z)

The transcript component of Z is a rectangle: two samples in the same Z fiber also contain the two mixed input pairs in that transcript rectangle.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialCoordinate_eq_of_same_zVariable (n : ℕ+) (p : ProtocolType n) {z : ZType n p} {ω ω' : HardSample n} (hω : zVariable n p ω = z) (hω' : zVariable n p ω' = z) : ω.T = ω'.T

Two samples in the same Z fiber have the same special coordinate.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBeforeSpecial_eq_of_same_zVariable (n : ℕ+) (p : ProtocolType n) {z : ZType n p} {ω ω' : HardSample n} (hω : zVariable n p ω = z) (hω' : zVariable n p ω' = z) : xBeforeSpecial n ω = xBeforeSpecial n ω'

Two samples in the same Z fiber have the same X_<T conditioning data.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yAfterSpecial_eq_of_same_zVariable (n : ℕ+) (p : ProtocolType n) {z : ZType n p} {ω ω' : HardSample n} (hω : zVariable n p ω = z) (hω' : zVariable n p ω' = z) : yAfterSpecial n ω = yAfterSpecial n ω'

Two samples in the same Z fiber have the same Y_>T conditioning data.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zVariable_mix_eq_of_same_zVariable (n : ℕ+) (p : ProtocolType n) {z : ZType n p} {ωX ωY : HardSample n} (hωX : zVariable n p ωX = z) (hωY : zVariable n p ωY = z) : zVariable n p (mix n ωX ωY) = z

The mixed sample of two samples in the same Z fiber remains in that Z fiber.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.mix_mem_fiber_inter_specialPair_of_mem_specialX_specialY (n : ℕ+) (p : ProtocolType n) {z : ZType n p} {ωX ωY : HardSample n} {bX bY : Bool} (hωX : ωX ∈ zFiber n p z ∩ specialX n ⁻¹' {bX}) (hωY : ωY ∈ zFiber n p z ∩ specialY n ⁻¹' {bY}) : mix n ωX ωY ∈ zFiber n p z ∩ specialPair n ⁻¹' {(bX, bY)}

If two samples are in a Z=z fiber, and the first has Alice special bit bX while the second has Bob special bit bY, then their mix is in the same fiber with special pair (bX, bY).

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.mix_swap_mem_fiber_of_mem_specialX_specialY (n : ℕ+) (p : ProtocolType n) {z : ZType n p} {ωX ωY : HardSample n} {bX bY : Bool} (hωX : ωX ∈ zFiber n p z ∩ specialX n ⁻¹' {bX}) (hωY : ωY ∈ zFiber n p z ∩ specialY n ⁻¹' {bY}) : mix n ωY ωX ∈ zFiber n p z

The swapped mix of two samples in a Z=z fiber remains in that fiber.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.mix_mem_fiber_inter_specialX_of_mem_specialPair_fiber (n : ℕ+) (p : ProtocolType n) {z : ZType n p} {ωPair ω : HardSample n} {b : Bool × Bool} (hωPair : ωPair ∈ zFiber n p z ∩ specialPair n ⁻¹' {b}) (hω : ω ∈ zFiber n p z) : mix n ωPair ω ∈ zFiber n p z ∩ specialX n ⁻¹' {b.1}

If one sample in a fiber has special pair b and the other is just in the fiber, mixing with the special-pair sample on Alice's side lands in the fiber with Alice special bit b.1.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.mix_mem_fiber_inter_specialY_of_mem_fiber_specialPair (n : ℕ+) (p : ProtocolType n) {z : ZType n p} {ωPair ω : HardSample n} {b : Bool × Bool} (hω : ω ∈ zFiber n p z) (hωPair : ωPair ∈ zFiber n p z ∩ specialPair n ⁻¹' {b}) : mix n ω ωPair ∈ zFiber n p z ∩ specialY n ⁻¹' {b.2}

If one sample in a fiber has special pair b and the other is just in the fiber, mixing with the special-pair sample on Bob's side lands in the fiber with Bob special bit b.2.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.card_fiber_inter_specialX_mul_card_fiber_inter_specialY (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (b : Bool × Bool) : Fintype.card { ω : HardSample n // ω ∈ zFiber n p z ∩ specialX n ⁻¹' {b.1} } * Fintype.card { ω : HardSample n // ω ∈ zFiber n p z ∩ specialY n ⁻¹' {b.2} } = Fintype.card { ω : HardSample n // ω ∈ zFiber n p z ∩ specialPair n ⁻¹' {b} } * Fintype.card { ω : HardSample n // ω ∈ zFiber n p z }

The switching map (ωX, ωY) ↦ (mix ωX ωY, mix ωY ωX) gives the cardinal identity underlying conditional independence of specialX and specialY on a Z=z fiber.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.measureReal_eq_card_subtype_div (n : ℕ+) (S : Set (HardSample n)) : MeasureTheory.volume.real S = ↑(Fintype.card { ω : HardSample n // ω ∈ S }) / ↑(Fintype.card (HardSample n))

Under the uniform hard-distribution measure, real measure is cardinality divided by the size of the sample space.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fiber_volume_factorization (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (b : Bool × Bool) : MeasureTheory.volume.real (zFiber n p z) * MeasureTheory.volume.real (zFiber n p z ∩ specialPair n ⁻¹' {b}) = MeasureTheory.volume.real (zFiber n p z ∩ specialX n ⁻¹' {b.1}) * MeasureTheory.volume.real (zFiber n p z ∩ specialY n ⁻¹' {b.2})

The rectangle switching identity, translated from cardinalities to the uniform hard-distribution measure.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.conditionalSpecialPairLaw_eq_prod_of_singleton_factorization (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (hfactor : ∀ (b : Bool × Bool), (↑(conditionalSpecialPairLaw n p z)).real {b} = (↑(conditionalSpecialXLaw n p z)).real {b.1} * (↑(conditionalSpecialYLaw n p z)).real {b.2}) : conditionalSpecialPairLaw n p z = TVDistance.probabilityMeasureProd (conditionalSpecialXLaw n p z) (conditionalSpecialYLaw n p z)

To prove the conditional special-pair law factors, it suffices to prove singleton factorization for the four bit-pairs.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.conditionalSpecialPairLaw_eq_prod_of_zFiberMeasure_factorization (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (hfactor : ∀ (b : Bool × Bool), (zFiberMeasure n p z).real (specialPair n ⁻¹' {b}) = (zFiberMeasure n p z).real (specialX n ⁻¹' {b.1}) * (zFiberMeasure n p z).real (specialY n ⁻¹' {b.2})) : conditionalSpecialPairLaw n p z = TVDistance.probabilityMeasureProd (conditionalSpecialXLaw n p z) (conditionalSpecialYLaw n p z)

Singleton factorization can be proved directly on the underlying Z=z fiber measure.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.conditionalSpecialPairLaw_eq_prod_of_fiber_volume_factorization (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (hfactor : ∀ (b : Bool × Bool), MeasureTheory.volume.real (zFiber n p z) * MeasureTheory.volume.real (zFiber n p z ∩ specialPair n ⁻¹' {b}) = MeasureTheory.volume.real (zFiber n p z ∩ specialX n ⁻¹' {b.1}) * MeasureTheory.volume.real (zFiber n p z ∩ specialY n ⁻¹' {b.2})) : conditionalSpecialPairLaw n p z = TVDistance.probabilityMeasureProd (conditionalSpecialXLaw n p z) (conditionalSpecialYLaw n p z)

A cross-multiplied version of singleton factorization, phrased using the original hard distribution instead of conditional fiber probabilities.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.conditionalSpecialPairLaw_eq_prod (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : conditionalSpecialPairLaw n p z = TVDistance.probabilityMeasureProd (conditionalSpecialXLaw n p z) (conditionalSpecialYLaw n p z)

The protocol transcript is a rectangle on each coarse fiber, so conditioned on a positive Z=z fiber the special bits factor as the product of their two marginals.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.conditionalSpecialPairLaw_singleton_factorization_of_eq_prod (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (hprod : conditionalSpecialPairLaw n p z = TVDistance.probabilityMeasureProd (conditionalSpecialXLaw n p z) (conditionalSpecialYLaw n p z)) (b : Bool × Bool) : (↑(conditionalSpecialPairLaw n p z)).real {b} = (↑(conditionalSpecialXLaw n p z)).real {b.1} * (↑(conditionalSpecialYLaw n p z)).real {b.2}

A product special-pair law gives singleton factorization of the conditional bit laws on the same Z fiber.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.conditionalSpecialXLaw_eq_cond_specialY_of_prod (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (hprod : conditionalSpecialPairLaw n p z = TVDistance.probabilityMeasureProd (conditionalSpecialXLaw n p z) (conditionalSpecialYLaw n p z)) (bY : Bool) (hY : (zFiberMeasure n p z).real (specialY n ⁻¹' {bY}) ≠ 0) : conditionalSpecialXLaw n p z = MeasureTheory.ProbabilityMeasure.map ⟨(zFiberMeasure n p z)[|specialY n ⁻¹' {bY}], ⋯⟩ ⋯

On a product-law Z fiber, conditioning on one Bob special-bit value does not change Alice's special-bit law.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.conditionalSpecialXLaw_eq_cond_specialYFalse (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (hY : (zFiberMeasure n p z).real (specialY n ⁻¹' {false}) ≠ 0) : conditionalSpecialXLaw n p z = MeasureTheory.ProbabilityMeasure.map ⟨(zFiberMeasure n p z)[|specialY n ⁻¹' {false}], ⋯⟩ ⋯

Rectangle switching implies the textbook fiber identity p(X_T | Z=z) = p(X_T | Z=z, Y_T=false).

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xFiberKL_eq_cond_specialYFalse_klDiv (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (hY : (zFiberMeasure n p z).real (specialY n ⁻¹' {false}) ≠ 0) : xFiberKL n p z = (InformationTheory.klDiv ↑(MeasureTheory.ProbabilityMeasure.map ⟨(zFiberMeasure n p z)[|specialY n ⁻¹' {false}], ⋯⟩ ⋯) ↑uniformBool).toReal

After rectangle switching, Alice's xFiberKL can be computed by first conditioning on Y_T=false inside the Z=z fiber.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xFiberKL_eq_disjointSpecialYFalseMeasure_cond_zVariable_klDiv (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (hY : (zFiberMeasure n p z).real (specialY n ⁻¹' {false}) ≠ 0) : xFiberKL n p z = (InformationTheory.klDiv (MeasureTheory.Measure.map (specialX n) (disjointSpecialYFalseMeasure n)[|zVariable n p ⁻¹' {z}]) ↑uniformBool).toReal

Alice's xFiberKL can be rewritten as KL for the special Alice bit under D ∧ Y_T=false conditioned on the same Z=z fiber.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xFiberKL_eq_disjointSpecialYFalseMeasure_cond_zVariable_klDiv_of_ne_zero (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (hz : (disjointSpecialYFalseMeasure n).real (zFiber n p z) ≠ 0) : xFiberKL n p z = (InformationTheory.klDiv (MeasureTheory.Measure.map (specialX n) (disjointSpecialYFalseMeasure n)[|zVariable n p ⁻¹' {z}]) ↑uniformBool).toReal

Positive mass under D ∧ Y_T=false supplies the positivity hypotheses needed to rewrite Alice's fiber KL using the D ∧ Y_T=false, Z=z conditional law.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zDistance_le_xDistance_add_yDistance (n : ℕ+) (p : ProtocolType n) (z : ZType n p) : zDistance n p z ≤ xDistance n p z + yDistance n p z

Product-distribution step in Lemma 6.22 for Z fibers. This uses the textbook rectangle fact: conditioned on a transcript rectangle and the coarse data, the special bits are independent, so the pair TV distance is controlled by the two one-bit TV distances.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.mem_goodZEvent_of_xDistance_yDistance_le (n : ℕ+) (p : ProtocolType n) {γ : ℝ} {ω : HardSample n} (hx : xDistance n p (zVariable n p ω) ≤ γ) (hy : yDistance n p (zVariable n p ω) ≤ γ) : ω ∈ goodZEvent n p γ

If both one-bit marginal distances on a Z fiber are at most γ, then the fiber is good.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceInfoTerm (n : ℕ+) (p : ProtocolType n) : ℝ

The corrected Alice information term in (6.6): I(X_T : M | T, X_<T, Y_≥T, D).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.bobInfoTerm (n : ℕ+) (p : ProtocolType n) : ℝ

The corrected Bob information term in (6.6): I(Y_T : M | T, X_≤T, Y_>T, D).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.claimInfo (n : ℕ+) (p : ProtocolType n) : ℝ

The total corrected special-coordinate information from (6.6).

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.bobInfoTerm_nonneg (n : ℕ+) (p : ProtocolType n) : 0 ≤ bobInfoTerm n p

Bob's corrected information term is nonnegative.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceInfoTerm_le_claimInfo (n : ℕ+) (p : ProtocolType n) : aliceInfoTerm n p ≤ claimInfo n p

Alice's information term is bounded by the total corrected information.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceInfoTerm_dualProtocol_eq_bobInfoTerm (n : ℕ+) (p : ProtocolType n) : aliceInfoTerm n (dualProtocol n p) = bobInfoTerm n p

Alice's corrected information term for the dual protocol is Bob's corrected information term for the original protocol.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.bobInfoTerm_dualProtocol_eq_aliceInfoTerm (n : ℕ+) (p : ProtocolType n) : bobInfoTerm n (dualProtocol n p) = aliceInfoTerm n p

Bob's corrected information term for the dual protocol is Alice's corrected information term for the original protocol.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xVector_message_info_dualProtocol_eq_yVector_message_info (n : ℕ+) (p : ProtocolType n) : I[xVector n : message n (dualProtocol n p)|yVector n;disjointCondMeasure n] = I[yVector n : message n p|xVector n;disjointCondMeasure n]

Full-vector information for the dual protocol is the swapped full-vector information for the original protocol.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.claimInfo_dualProtocol (n : ℕ+) (p : ProtocolType n) : claimInfo n (dualProtocol n p) = claimInfo n p

The total corrected information is invariant under protocol duality.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedAliceInfoTerm (n : ℕ+) (p : ProtocolType n) (i : Fin ↑n) : ℝ

The fixed-coordinate summand I(X_i : M | X_<i, Y_≥i) in Lemma 6.20.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedAliceFullYInfoTerm (n : ℕ+) (p : ProtocolType n) (i : Fin ↑n) : ℝ

The fixed-coordinate term with the full Y vector in the conditioning.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedAliceCrossInfoTerm (n : ℕ+) (i : Fin ↑n) : ℝ

The zero cross-information term I(X_i : Y_<i | X_<i, Y_≥i) in Lemma 6.20.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedAliceCrossInfoTerm_eq_zero (n : ℕ+) (i : Fin ↑n) : fixedAliceCrossInfoTerm n i = 0

Textbook Lemma 6.20 independence input for the hard distribution conditioned on D: I(X_i : Y_<i | X_<i, Y_≥i, D) = 0.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixedAliceInfoTerm_le_fixedAliceFullYInfoTerm (n : ℕ+) (p : ProtocolType n) (i : Fin ↑n) : fixedAliceInfoTerm n p i ≤ fixedAliceFullYInfoTerm n p i

Fixed-coordinate chain-rule inequality from Lemma 6.20: I(X_i : M | X_<i,Y_≥i) ≤ I(X_i : M | X_<i,Y).

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.sum_fixedAliceInfoTerm_le_sum_fixedAliceFullYInfoTerm (n : ℕ+) (p : ProtocolType n) : ∑ i : Fin ↑n, fixedAliceInfoTerm n p i ≤ ∑ i : Fin ↑n, fixedAliceFullYInfoTerm n p i

Summing the fixed-coordinate inequalities from Lemma 6.20.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.sum_fixedAliceFullYInfoTerm_eq_xVector_info (n : ℕ+) (p : ProtocolType n) : ∑ i : Fin ↑n, fixedAliceFullYInfoTerm n p i = I[xVector n : message n p|yVector n;disjointCondMeasure n]

Textbook chain rule for the full Alice vector: ∑ᵢ I(X_i : M | X_<i,Y,D) = I(X : M | Y,D).

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.sum_fixedAliceInfoTerm_le_xVector_info (n : ℕ+) (p : ProtocolType n) : ∑ i : Fin ↑n, fixedAliceInfoTerm n p i ≤ I[xVector n : message n p|yVector n;disjointCondMeasure n]

Textbook Lemma 6.20 chain-rule step for the Alice summands: ∑ᵢ I(X_i : M | X_<i, Y_≥i, D) ≤ I(X : M | Y, D).

This is the proof-specific instance of Lemma 6.20; its only probabilistic input is fixedAliceCrossInfoTerm_eq_zero.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceInfoTerm_eq_sum_specialCoordinate_fiber_info (n : ℕ+) (p : ProtocolType n) : aliceInfoTerm n p = ∑ i : Fin ↑n, 1 / ↑↑n * I[specialX n : message n p|aliceDynamicConditioning n;(disjointCondMeasure n)[|specialCoordinate n ⁻¹' {i}]]

Expanding Alice's random-coordinate information term by the special coordinate T.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceDynamicConditioning_fiber_info_eq_fixedAliceInfoTerm (n : ℕ+) (p : ProtocolType n) (i : Fin ↑n) : I[specialX n : message n p|aliceDynamicConditioning n;(disjointCondMeasure n)[|specialCoordinate n ⁻¹' {i}]] = fixedAliceInfoTerm n p i

Textbook uniformity/independence step for the special coordinate: after conditioning on T=i, the random-coordinate Alice information term is the fixed-coordinate summand.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceInfoTerm_eq_average_fixedAliceInfoTerm (n : ℕ+) (p : ProtocolType n) : aliceInfoTerm n p = (∑ i : Fin ↑n, fixedAliceInfoTerm n p i) / ↑↑n

Averaging over the special coordinate: conditioned on D, T is uniform and independent of (X,Y,M), so the Alice term in (6.6) is the average of the fixed-coordinate Lemma 6.20 summands.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceInfoTerm_le_average_xVector_info (n : ℕ+) (p : ProtocolType n) : aliceInfoTerm n p ≤ I[xVector n : message n p|yVector n;disjointCondMeasure n] / ↑↑n

Alice half of Lemma 6.20, after conditioning on disjointness and averaging over the uniform special coordinate: I(X_T : M | T, X_<T, Y_≥T, D) ≤ I(X : M | Y, D) / n.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.bobInfoTerm_le_average_yVector_info (n : ℕ+) (p : ProtocolType n) : bobInfoTerm n p ≤ I[yVector n : message n p|xVector n;disjointCondMeasure n] / ↑↑n

Bob half of Lemma 6.20, after conditioning on disjointness and averaging over the uniform special coordinate: I(Y_T : M | T, X_≤T, Y_>T, D) ≤ I(Y : M | X, D) / n.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xVector_message_info_le_complexity_mul_log_two (n : ℕ+) (p : ProtocolType n) : I[xVector n : message n p|yVector n;disjointCondMeasure n] ≤ ↑(Deterministic.Protocol.complexity p) * Real.log 2

The Alice full-vector information is bounded by the transcript entropy.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yVector_message_info_le_complexity_mul_log_two (n : ℕ+) (p : ProtocolType n) : I[yVector n : message n p|xVector n;disjointCondMeasure n] ≤ ↑(Deterministic.Protocol.complexity p) * Real.log 2

The Bob full-vector information is bounded by the transcript entropy.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceInfoTerm_le_average_entropy_bound (n : ℕ+) (p : ProtocolType n) : aliceInfoTerm n p ≤ ↑(Deterministic.Protocol.complexity p) * Real.log 2 / ↑↑n

Alice half of Lemma 6.20 plus the entropy bound H(M) ≤ ℓ, averaged over the uniform special coordinate.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.bobInfoTerm_le_average_entropy_bound (n : ℕ+) (p : ProtocolType n) : bobInfoTerm n p ≤ ↑(Deterministic.Protocol.complexity p) * Real.log 2 / ↑↑n

Bob half of Lemma 6.20 plus the entropy bound H(M) ≤ ℓ, averaged over the uniform special coordinate.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.claimInfo_le_average_info_upper (n : ℕ+) (p : ProtocolType n) : claimInfo n p ≤ 2 * (↑(Deterministic.Protocol.complexity p) * Real.log 2) / ↑↑n

Lemma 6.20 plus the entropy bound H(M) ≤ ℓ: the corrected claim information is at most the averaged full-vector transcript information. This is the part before (6.6) in .codex/disjointness.txt.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yGeSpecial_eq_yAfterSpecial_of_specialY_false (n : ℕ+) {ω : HardSample n} (hY : specialY n ω = false) : yGeSpecial n ω = yAfterSpecial n ω

On the branch Y_T=false, the corrected Alice suffix Y_≥T is the same information as the coarse suffix Y_>T, since the missing coordinate is fixed to false.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceClaimConditioning_eq_coarseConditioning_of_specialY_false (n : ℕ+) {ω : HardSample n} (hY : specialY n ω = false) : aliceClaimConditioning n ω = coarseConditioning n ω

On the branch Y_T=false, Alice's corrected Claim 6.21 conditioning is exactly the coarse conditioning from the textbook Z=(M,T,X_<T,Y_>T).

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointSpecialYFalseMeasure_ae_specialY_false (n : ℕ+) : ∀ᵐ (ω : HardSample n) ∂disjointSpecialYFalseMeasure n, specialY n ω = false

Under D ∧ Y_T=false, Bob's special bit is almost surely false.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceClaimConditioning_ae_eq_coarseConditioning_disjointSpecialYFalse (n : ℕ+) : aliceClaimConditioning n =ᵐ[disjointSpecialYFalseMeasure n] coarseConditioning n

Under D ∧ Y_T=false, Alice's fine conditioning variable is a.e. the coarse conditioning variable.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceInfoTermSpecialYFalse (n : ℕ+) (p : ProtocolType n) : ℝ

The Claim 6.21 Alice information term after additionally conditioning on Y_T=false: I(X_T : M | T, X_<T, Y_≥T, Y_T=0, D).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceCoarseInfoTermSpecialYFalse (n : ℕ+) (p : ProtocolType n) : ℝ

The same Alice Y_T=false information term using the textbook coarse conditioning T, X_<T, Y_>T.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.condKLDiv_specialX_zVariable_eq_mutualInfo_zVariable (n : ℕ+) (p : ProtocolType n) : KL[specialX n | zVariable n p ; disjointSpecialYFalseMeasure n # id ; ↑uniformBool] = I[specialX n : zVariable n p ; disjointSpecialYFalseMeasure n]

Since X_T is uniform under D ∧ Y_T=false, the conditional KL average to the uniform bit law is the mutual information between X_T and the full Z=(M,T,X_<T,Y_>T) variable.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.aliceInfoTermSpecialYFalse_eq_aliceCoarseInfoTermSpecialYFalse (n : ℕ+) (p : ProtocolType n) : aliceInfoTermSpecialYFalse n p = aliceCoarseInfoTermSpecialYFalse n p

The fine Y_≥T and coarse Y_>T versions of the Alice Y_T=false information term agree, because Y_T is fixed on the conditioned measure.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.integral_xFiberKL_disjointSpecialYFalse_eq_sum_zVariable (n : ℕ+) (p : ProtocolType n) : ∫ (ω : HardSample n), xFiberKL n p (zVariable n p ω) ∂disjointSpecialYFalseMeasure n = ∑ z : ZType n p, (disjointSpecialYFalseMeasure n).real (zFiber n p z) * xFiberKL n p z

The averaged Alice fiber KL cost under D ∧ Y_T=false, as a finite sum over Z values.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.integral_xFiberKL_disjointSpecialYFalse_eq_sum_zVariable_klDiv (n : ℕ+) (p : ProtocolType n) : ∫ (ω : HardSample n), xFiberKL n p (zVariable n p ω) ∂disjointSpecialYFalseMeasure n = ∑ z : ZType n p, (disjointSpecialYFalseMeasure n).real (zFiber n p z) * (InformationTheory.klDiv (MeasureTheory.Measure.map (specialX n) (disjointSpecialYFalseMeasure n)[|zVariable n p ⁻¹' {z}]) ↑uniformBool).toReal

The averaged Alice fiber KL cost under D ∧ Y_T=false as a finite sum of actual KL divergences for the conditional Z=z laws.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.integral_xFiberKL_disjointSpecialYFalse_eq_condKLDiv_zVariable (n : ℕ+) (p : ProtocolType n) : ∫ (ω : HardSample n), xFiberKL n p (zVariable n p ω) ∂disjointSpecialYFalseMeasure n = KL[specialX n | zVariable n p ; disjointSpecialYFalseMeasure n # id ; ↑uniformBool]

The averaged Alice fiber KL under D ∧ Y_T=false, rewritten as the PFR real conditional KL used by the entropy API.

def CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.flipSpecialX (n : ℕ+) (ω : HardSample n) : HardSample n

Flip only Alice's special-coordinate bit. This preserves the coarse Claim 6.21 data T, X_<T, Y_>T and toggles X_T.

Equations

• CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.flipSpecialX n ω = { T := ω.T, xT := !ω.xT, yT := ω.yT, other := ω.other }

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.flipSpecialX_flipSpecialX (n : ℕ+) (ω : HardSample n) : flipSpecialX n (flipSpecialX n ω) = ω

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.flipSpecialX_preimage_singleton (n : ℕ+) (ω : HardSample n) : flipSpecialX n ⁻¹' {ω} = {flipSpecialX n ω}

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.volume_measureReal_singleton_flipSpecialX (n : ℕ+) (ω : HardSample n) : MeasureTheory.volume.real {flipSpecialX n ω} = MeasureTheory.volume.real {ω}

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.volume_measurePreserving_flipSpecialX (n : ℕ+) : MeasureTheory.MeasurePreserving (flipSpecialX n) MeasureTheory.volume MeasureTheory.volume

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialX_flipSpecialX (n : ℕ+) (ω : HardSample n) : specialX n (flipSpecialX n ω) = !specialX n ω

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.specialY_flipSpecialX (n : ℕ+) (ω : HardSample n) : specialY n (flipSpecialX n ω) = specialY n ω

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xBeforeSpecial_flipSpecialX (n : ℕ+) (ω : HardSample n) : xBeforeSpecial n (flipSpecialX n ω) = xBeforeSpecial n ω

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.yAfterSpecial_flipSpecialX (n : ℕ+) (ω : HardSample n) : yAfterSpecial n (flipSpecialX n ω) = yAfterSpecial n ω

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.coarseConditioning_flipSpecialX (n : ℕ+) (ω : HardSample n) : coarseConditioning n (flipSpecialX n ω) = coarseConditioning n ω

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.volume_measureReal_specialYFalse_inter_coarseConditioning_inter_specialX (n : ℕ+) (b : Bool) (c : Fin ↑n × (Fin ↑n → Bool) × (Fin ↑n → Bool)) : MeasureTheory.volume.real (specialY n ⁻¹' {false} ∩ coarseConditioning n ⁻¹' {c} ∩ specialX n ⁻¹' {b}) = 1 / 2 * MeasureTheory.volume.real (specialY n ⁻¹' {false} ∩ coarseConditioning n ⁻¹' {c})

In every Y_T=false, coarse=c fiber of the ambient hard distribution, each value of X_T has half the mass.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.disjointSpecialYFalseMeasure_measureReal_specialX_inter_coarseConditioning (n : ℕ+) (b : Bool) (c : Fin ↑n × (Fin ↑n → Bool) × (Fin ↑n → Bool)) : (disjointSpecialYFalseMeasure n).real (specialX n ⁻¹' {b} ∩ coarseConditioning n ⁻¹' {c}) = 1 / 2 * (disjointSpecialYFalseMeasure n).real (coarseConditioning n ⁻¹' {c})

The preceding ambient counting identity remains true after conditioning on Y_T=false.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.mutualInfo_specialX_coarseConditioning_disjointSpecialYFalse_eq_zero (n : ℕ+) : I[specialX n : coarseConditioning n ; disjointSpecialYFalseMeasure n] = 0

Under D ∧ Y_T=false, the coarse data T, X_<T, Y_>T is independent of X_T. This is the sampling independence used in Claim 6.21 before adding the transcript rectangle.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.mutualInfo_specialX_zVariable_eq_aliceCoarseInfoTermSpecialYFalse (n : ℕ+) (p : ProtocolType n) : I[specialX n : zVariable n p ; disjointSpecialYFalseMeasure n] = aliceCoarseInfoTermSpecialYFalse n p

The full Z=(M,coarse) mutual information is the coarse Claim 6.21 information term, because the coarse part alone is independent of X_T under D ∧ Y_T=false.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xFiberKL_integral_eq_aliceCoarseInfoTermSpecialYFalse (n : ℕ+) (p : ProtocolType n) : ∫ (ω : HardSample n), xFiberKL n p (zVariable n p ω) ∂disjointSpecialYFalseMeasure n = aliceCoarseInfoTermSpecialYFalse n p

Textbook Claim 6.21 KL identification with the coarse Z conditioning: the average Alice one-bit fiber KL is the conditional mutual information I(X_T : M | T,X_<T,Y_>T,Y_T=0,D).

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.xFiberKL_integral_eq_aliceInfoTermSpecialYFalse (n : ℕ+) (p : ProtocolType n) : ∫ (ω : HardSample n), xFiberKL n p (zVariable n p ω) ∂disjointSpecialYFalseMeasure n = aliceInfoTermSpecialYFalse n p

Textbook Claim 6.21 identification of the average Alice one-bit fiber KL with the conditional mutual information under Y_T=false. This packages the step p(x_t | z) = p(x_t | z, y_t=0) = p(x_t | z, y_t=0, D) coming from independence and the rectangle property of the transcript.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.two_thirds_mul_aliceInfoTermSpecialYFalse_le_aliceInfoTerm (n : ℕ+) (p : ProtocolType n) : 2 / 3 * aliceInfoTermSpecialYFalse n p ≤ aliceInfoTerm n p

Textbook Claim 6.21 reweighting: (2/3) I(X_T : M | T, X_< T, Y_≥T, Y_T=0, D) ≤ I(X_T : M | T, X_< T, Y_≥T, D).

The factor is Pr[Y_T=false | D] = 2/3, and the event Y_T=false is determined by the conditioning variable because Y_≥T contains Y_T.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.claim621_x_fiberKL_disjointSpecialYFalse_le_three_halves_aliceInfoTerm (n : ℕ+) (p : ProtocolType n) : ∫ (ω : HardSample n), xFiberKL n p (zVariable n p ω) ∂disjointSpecialYFalseMeasure n ≤ 3 / 2 * aliceInfoTerm n p

Textbook Claim 6.21, Alice information step under D ∧ Y_T=false: the average one-bit KL cost is bounded by Alice's term from (6.6), with the 2/3 conditioning factor.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.claim621_x_fiberKL_disjointSpecialYFalse_le (n : ℕ+) (p : ProtocolType n) {γ : ℝ} (hγ : 0 < γ) (hinfo : claimInfo n p ≤ 2 * γ ^ 4 / 3) : ∫ (ω : HardSample n), xFiberKL n p (zVariable n p ω) ∂disjointSpecialYFalseMeasure n ≤ 2 * γ ^ 4

Textbook Claim 6.21, Alice information step under D ∧ Y_T=false: the average one-bit KL cost is bounded by the small total information assumption.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.claim621_x_average_sq_distance_disjointSpecialYFalse_le (n : ℕ+) (p : ProtocolType n) {γ : ℝ} (hγ : 0 < γ) (hinfo : claimInfo n p ≤ 2 * γ ^ 4 / 3) : ∫ (ω : HardSample n), xDistance n p (zVariable n p ω) ^ 2 ∂disjointSpecialYFalseMeasure n ≤ γ ^ 4

Textbook Claim 6.21, Alice Pinsker/information step under D ∧ Y_T=false: the squared one-bit marginal distance has average at most γ^4. This is the KL-to-information comparison from the displayed (2/3) I(X_T : M | T, X_<T, Y_≥T, Y_T=0, D) ≤ I(X_T : M | T, X_<T, Y_≥T, D).

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.claim621_x_bad_on_specialZeroZero_le (n : ℕ+) (p : ProtocolType n) {γ : ℝ} (hγ : 0 < γ) (hinfo : claimInfo n p ≤ 2 * γ ^ 4 / 3) : MeasureTheory.volume.real (specialZeroZero n ∩ {ω : HardSample n | γ < xDistance n p (zVariable n p ω)}) ≤ γ / 2

Alice marginal part of Claim 6.21: under the (X_T,Y_T)=(0,0) slice, the set of Z fibers whose Alice special-bit marginal is farther than γ from uniform has mass at most γ / 2.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.claim621_y_bad_on_specialZeroZero_le (n : ℕ+) (p : ProtocolType n) {γ : ℝ} (hγ : 0 < γ) (hinfo : claimInfo n p ≤ 2 * γ ^ 4 / 3) : MeasureTheory.volume.real (specialZeroZero n ∩ {ω : HardSample n | γ < yDistance n p (zVariable n p ω)}) ≤ γ / 2

Bob marginal part of Claim 6.21, symmetric to the Alice marginal estimate.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.textbook_claim_6_21 (n : ℕ+) (p : ProtocolType n) {γ : ℝ} (hγ : 0 < γ) (hinfo : claimInfo n p ≤ 2 * γ ^ 4 / 3) : 1 / 4 * (1 - 4 * γ) ≤ MeasureTheory.volume.real (goodZEvent n p γ)

Claim 6.21 in the corrected transcription. If the corrected information from (6.6) is ≤ 2γ^4 / 3, then the set of Z fibers where the conditional law of (X_T, Y_T) is within 2γ of uniform has hard-distribution mass at least (1 - 4γ) / 4.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zFiberMeasure_inter_fiber (n : ℕ+) (p : ProtocolType n) (z : ZType n p) (S : Set (HardSample n)) : (zFiberMeasure n p z).real (zFiber n p z ∩ S) = (zFiberMeasure n p z).real S

Intersecting with the defining Z=z fiber does not change probabilities under the corresponding fiber measure.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.abs_conditionalSpecialPairLaw_singleton_sub_quarter_le (n : ℕ+) (p : ProtocolType n) {γ : ℝ} {z : ZType n p} (hgood : goodZ n p γ z) (b : Bool × Bool) : |(↑(conditionalSpecialPairLaw n p z)).real {b} - 1 / 4| ≤ 2 * γ

A good z gives the expected singleton-mass estimate for the conditional special-pair law.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.quarter_sub_two_mul_le_conditionalSpecialPairLaw_singleton (n : ℕ+) (p : ProtocolType n) {γ : ℝ} {z : ZType n p} (hgood : goodZ n p γ z) (b : Bool × Bool) : 1 / 4 - 2 * γ ≤ (↑(conditionalSpecialPairLaw n p z)).real {b}

A good z gives a lower bound on each singleton mass of the conditional special-pair law.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.zFiber_inter_diag_specialPair_subset_protocolErrorEvent (n : ℕ+) (p : ProtocolType n) {z : ZType n p} : zFiber n p z ∩ specialPair n ⁻¹' {(zOutput n p z, zOutput n p z)} ⊆ protocolErrorEvent n p

On a fixed Z=z fiber, inputs whose special pair equals the Z-determined protocol output on both sides are protocol errors.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.quarter_sub_two_mul_le_zFiberMeasure_protocolErrorEvent (n : ℕ+) (p : ProtocolType n) {γ : ℝ} {z : ZType n p} (hgood : goodZ n p γ z) : 1 / 4 - 2 * γ ≤ (zFiberMeasure n p z).real (protocolErrorEvent n p)

On a good Z fiber, the conditional protocol-error probability is at least 1 / 4 - 2 * γ. If the protocol output on the fiber is true, then the (true, true) special bit-pair witnesses errors; otherwise (false, false) witnesses errors.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.goodZEvent_mul_quarter_sub_two_mul_le_protocolErrorEvent (n : ℕ+) (p : ProtocolType n) (γ : ℝ) : MeasureTheory.volume.real (goodZEvent n p γ) * (1 / 4 - 2 * γ) ≤ MeasureTheory.volume.real (protocolErrorEvent n p)

Averaging the good-fiber error lower bound over all good Z fibers gives an unconditional error lower bound.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.distributionalError_lower_bound_of_goodZEvent (n : ℕ+) (p : ProtocolType n) (γ : ℝ) : MeasureTheory.volume.real (goodZEvent n p γ) * (1 / 4 - 2 * γ) ≤ Deterministic.Protocol.distributionalError p (inputDist n) (disjointness ↑n)

The final error calculation after Claim 6.21, phrased using distributional error.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.fixed_error_claimInfo_lower_bound (n : ℕ+) (p : ProtocolType n) (herror : Deterministic.Protocol.distributionalError p (inputDist n) (disjointness ↑n) ≤ 1 / 32) : (1 / 32768) ^ 2 < claimInfo n p

Textbook Claim 6.21 and the final error calculation: a deterministic protocol with distributional error at most 1 / 32 must reveal a constant amount of the corrected information from (6.6).

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.deterministic_complexity_lower_bound_textbook (n : ℕ+) (p : ProtocolType n) (herror : Deterministic.Protocol.distributionalError p (inputDist n) (disjointness ↑n) ≤ 1 / 32) : (1 / 32768) ^ 2 * ↑↑n / (3 * Real.log 2) ≤ ↑(Deterministic.Protocol.complexity p)

Deterministic fixed-error disjointness lower bound from (6.6) and Lemma 6.20.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.publicCoin_lower_bound_textbook (n : ℕ+) {k : ℕ} (hk : ↑k < (1 / 32768) ^ 2 * ↑↑n / (3 * Real.log 2)) : ↑k < PublicCoin.communicationComplexity (disjointness ↑n) (1 / 32)

Public-coin fixed-error lower bound from the textbook deterministic distributional lower bound via minimax.

theorem CommunicationComplexity.Functions.Disjointness.RandomizedLowerBound.publicCoin_communicationComplexity_disjointness_linear_lower_bound (n : ℕ+) : ↑⌊↑↑n / 2 ^ 32⌋₊ < PublicCoin.communicationComplexity (disjointness ↑n) (1 / 32)

Headline theorem: public-coin randomized communication complexity of disjointness is linear at fixed error 1 / 32, with a concrete conservative constant. The cutoff is the floor of the real number n / 2^32, so the asymptotic constant is stated over the reals.