General lemmas not specific to analysis of Boolean functions.

theorem LeanPool.LeanBooleanfun.BooleanFun.sum_singletons {α : Type u_1} {ι : Type u_2} [Fintype ι] [AddCommMonoid α] {F : Finset ι → α} {G : ι → α} (h : ∀ (i : ι), F {i} = G i) : ∑ S : Finset ι with S.card = 1, F S = ∑ i : ι, G i

theorem LeanPool.LeanBooleanfun.BooleanFun.sum_singletons' {α : Type u_1} {ι : Type u_2} [Fintype ι] [AddCommMonoid α] {F : Finset ι → α} : ∑ S : Finset ι with S.card = 1, F S = ∑ i : ι, F {i}

theorem LeanPool.LeanBooleanfun.BooleanFun.ite_ite_same {α : Type u_1} {P : Prop} [Decidable P] (a b c : α) : (if P then if P then a else b else c) = if P then a else c

theorem LeanPool.LeanBooleanfun.BooleanFun.rw_ite_left {α : Type u_1} {P : Prop} [Decidable P] {a b c : α} (h : P → a = c) : (if P then a else b) = if P then c else b

theorem LeanPool.LeanBooleanfun.BooleanFun.rw_ite_right {α : Type u_1} {P : Prop} [Decidable P] {a b c : α} (h : ¬P → a = c) : (if P then b else a) = if P then b else c

theorem LeanPool.LeanBooleanfun.BooleanFun.ite_add_ite {P : Prop} [Decidable P] {α : Type u_3} [AddCommMonoid α] (a₁ b₁ a₂ b₂ : α) : ((if P then a₁ else b₁) + if P then a₂ else b₂) = if P then a₁ + a₂ else b₁ + b₂

theorem LeanPool.LeanBooleanfun.BooleanFun.ite_ite_not {α : Type u_1} (P : Prop) [Decidable P] (a b c : α) : (if P then if ¬P then a else b else c) = if P then b else c

theorem LeanPool.LeanBooleanfun.BooleanFun.ite_ite_not' {α : Type u_1} (P : Prop) [Decidable P] (a b c : α) : (if ¬P then if P then a else b else c) = if ¬P then b else c

@[reducible, inline]

noncomputable abbrev LeanPool.LeanBooleanfun.BooleanFun.oneOn (p : Prop) : ℝ

Real-valued 0-1 indicator testing a proposition. We prefer this over using Set.indicator and we don't call it indicator to avoid overloading the Mathlib definition.

Equations

• LeanPool.LeanBooleanfun.BooleanFun.oneOn p = if p then 1 else 0

theorem LeanPool.LeanBooleanfun.BooleanFun.oneOn_true {p : Prop} (h : p) : oneOn p = 1

theorem LeanPool.LeanBooleanfun.BooleanFun.oneOn_false {p : Prop} (h : ¬p) : oneOn p = 0

theorem LeanPool.LeanBooleanfun.BooleanFun.oneOn_and {p q : Prop} : oneOn (p ∧ q) = oneOn p * oneOn q

theorem LeanPool.LeanBooleanfun.BooleanFun.oneOn_not {p : Prop} : (oneOn ¬p) = 1 - oneOn p

theorem LeanPool.LeanBooleanfun.BooleanFun.oneOn_prod {ι : Type u_2} [Fintype ι] {p : ι → Prop} : ∏ i : ι, oneOn (p i) = oneOn (∀ (i : ι), p i)

theorem LeanPool.LeanBooleanfun.BooleanFun.pow_eq_self_imp {ρ : ℝ} {k : ℕ} : ρ ^ k = ρ → k = 1 ∨ ρ = 0 ∨ ρ = 1 ∨ ρ = -1

Solutions of the equation ρᵏ = ρ in real numbers.