def OmegaCompletePartialOrder.ContinuousHom.lfp {a : Type u_1} [OmegaCompletePartialOrder a] [OrderBot a] (f : a →𝒄 a) : a

Equations

• f.lfp = OmegaCompletePartialOrder.ωSup { toFun := fun (n : ℕ) => (⇑f)^[n] ⊥, monotone' := ⋯ }

def GaudisCrypt.IsLfp {a : Type u_1} [LE a] (f : a → a) (x : a) : Prop

Equations

• GaudisCrypt.IsLfp f x = IsLeast (Function.fixedPoints f) x

theorem GaudisCrypt.ContinuousHom.lfp_isLfp {a : Type u_1} [OmegaCompletePartialOrder a] [OrderBot a] (f : a →𝒄 a) : IsLfp (⇑f) f.lfp

theorem GaudisCrypt.ContinuousHom.map_lfp_comp {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] [OrderBot α] [OrderBot β] (f : β →𝒄 α) (g : α →𝒄 β) : f (g.comp f).lfp = (f.comp g).lfp

@[simp]

theorem GaudisCrypt.ContinuousHom.map_lfp {a : Type u_1} [OmegaCompletePartialOrder a] [OrderBot a] (f : a →𝒄 a) : f f.lfp = f.lfp

theorem GaudisCrypt.lintegral_iSup_measure_nat {α : Type u_1} [MeasurableSpace α] {μ : ℕ → MeasureTheory.Measure α} (hmono : Monotone μ) {f : α → ENNReal} : ∫⁻ (a : α), f a ∂⨆ (n : ℕ), μ n = ⨆ (n : ℕ), ∫⁻ (a : α), f a ∂μ n

theorem GaudisCrypt.Bool.rec_ωScottContinuous {X : Type u_1} [OmegaCompletePartialOrder X] {α : Bool → Type u_2} [(b : Bool) → OmegaCompletePartialOrder (α b)] (a : Bool) {g : X → α false} {f : X → α true} (hg : OmegaCompletePartialOrder.ωScottContinuous g) (hf : OmegaCompletePartialOrder.ωScottContinuous f) : OmegaCompletePartialOrder.ωScottContinuous fun (x : X) => Bool.rec (g x) (f x) a

theorem GaudisCrypt.ite_ωScottContinuous {a : Type u_1} {b : Type u_2} [OmegaCompletePartialOrder a] [OmegaCompletePartialOrder b] (f g : a → b) (cond : Prop) [Decidable cond] (hg : OmegaCompletePartialOrder.ωScottContinuous g) (hf : OmegaCompletePartialOrder.ωScottContinuous f) : OmegaCompletePartialOrder.ωScottContinuous fun (x : a) => if cond then f x else g x

theorem GaudisCrypt.Bool.rec_monotone {X : Type u_1} [Preorder X] {α : Bool → Type u_2} [(b : Bool) → Preorder (α b)] (a : Bool) {g : X → α false} {f : X → α true} (hg : Monotone g) (hf : Monotone f) : Monotone fun (x : X) => Bool.rec (g x) (f x) a

def GaudisCrypt.OrderHom.ofFun {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α → β) (hf : Monotone f := by fun_prop) : α →o β

Equations

• GaudisCrypt.OrderHom.ofFun f hf = { toFun := f, monotone' := hf }

theorem GaudisCrypt.monotone_pi_apply {β : Type u_1} {α : Type u_2} [Preorder β] (i : α) : Monotone fun (f : α → β) => f i

theorem GaudisCrypt.monotone_pi {X : Type u_1} {ι : Type u_2} {A : ι → Type u_3} [Preorder X] [(i : ι) → Preorder (A i)] {f : X → (i : ι) → A i} (h : ∀ (i : ι), Monotone fun (a : X) => f a i) : Monotone f

theorem GaudisCrypt.monotone_ite {a : Type u_1} {b : Type u_2} (f g : a → b) [Preorder a] [Preorder b] (c : Prop) [Decidable c] (hf : Monotone f) (hg : Monotone g) : Monotone fun (x : a) => if c then f x else g x

theorem GaudisCrypt.monotone_comp {a : Type u_1} {b : Type u_2} {c : Type u_3} [Preorder a] [Preorder b] [Preorder c] {f : a → b} {g : c → a} : Monotone f → Monotone g → Monotone fun (x : c) => f (g x)

theorem GaudisCrypt.OrderHom.monotone_mk {a : Type u_1} {b : Type u_2} {c : Type u_3} [Preorder a] [Preorder b] [Preorder c] {f : a → b → c} (hinner : ∀ (x : a), Monotone (f x)) (hmono : ∀ (v : b), Monotone fun (x : a) => f x v) : Monotone fun (x : a) => { toFun := f x, monotone' := ⋯ }

theorem GaudisCrypt.monotone_fst' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Preorder X] [Preorder Y] [Preorder Z] (f : X → Y × Z) (hf : Monotone f) : Monotone fun (x : X) => (f x).1

theorem GaudisCrypt.monotone_snd' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Preorder X] [Preorder Y] [Preorder Z] (f : X → Y × Z) (hf : Monotone f) : Monotone fun (x : X) => (f x).2

theorem GaudisCrypt.monotone_prod_mk {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Preorder X] [Preorder Y] [Preorder Z] (f : X → Y) (g : X → Z) (hf : Monotone f) (hg : Monotone g) : Monotone fun (x : X) => (f x, g x)

theorem GaudisCrypt.monotone_ContinuousHom {a : Type u_1} {b : Type u_2} [OmegaCompletePartialOrder a] [OmegaCompletePartialOrder b] (f : a →𝒄 b) : Monotone fun (x : a) => f x

theorem GaudisCrypt.monotone_OrderHom_apply {a : Type u_1} {b : Type u_2} {c : Type u_3} [Preorder a] [Preorder b] [Preorder c] {f : a → b →o c} (hf : Monotone f) {g : a → b} (hg : Monotone g) : Monotone fun (x : a) => (f x) (g x)

theorem GaudisCrypt.OrderHom.lfp_monotone {c : Type u_1} [CompleteLattice c] : Monotone ⇑OrderHom.lfp

theorem GaudisCrypt.sum_indicator_eq_card_ENNReal {α : Type u_1} [Fintype α] [DecidableEq α] (S : Finset α) : (∑ y : α, if y ∈ S then 1 else 0) = ↑S.card

Sum of a 0/1 indicator over a finite type equals the size of the indicated set.

theorem GaudisCrypt.ENNReal.natCast_succ_sub_one (n : ℕ) : ↑(n + 1) - 1 = ↑n

((n + 1 : ℕ) : ENNReal) - 1 = (n : ENNReal) — the standard ℕ-cast successor cancellation in ENNReal (with truncated subtraction). Used pervasively in birthday-bound arithmetic.