structure CompactSubgroups.GroupBornology (G : Type u_3) [Group G] : Type u_3

A bornology on a group $G$: a family of bounded sets closed under taking subsets, finite unions, singletons, group products, and inversion.

• isBounded : Set G → Prop
• subset_bounded {S T : Set G} : self.isBounded T → S ⊆ T → self.isBounded S
• singleton_bounded (g : G) : self.isBounded {g}
• union_bounded {S T : Set G} : self.isBounded S → self.isBounded T → self.isBounded (S ∪ T)
• product_bounded {S T : Set G} : self.isBounded S → self.isBounded T → self.isBounded (setMul S T)
• inv_bounded {S : Set G} : self.isBounded S → self.isBounded ((fun (x : G) => x⁻¹) '' S)

def CompactSubgroups.IsBoundedSubgroup {G : Type u_1} [Group G] (born : GroupBornology G) (H : Subgroup G) : Prop

A subgroup $H$ is bounded in the bornology $\mathrm{born}$ if its underlying set is bounded.

def CompactSubgroups.IsMaximalBounded {G : Type u_1} [Group G] (born : GroupBornology G) (K : Subgroup G) : Prop

A subgroup $K$ is maximal bounded if it is bounded and no strictly larger subgroup is bounded.

def CompactSubgroups.BNPairBoundedPredicate {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (S : Set G) : Prop

$S$ is BN-pair bounded: covered by finitely many Bruhat cells of $\mathrm{bp}$.

theorem CompactSubgroups.bnpair_product_bounded {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (S T : Set G) (hS : BNPairBoundedPredicate bp S) (hT : BNPairBoundedPredicate bp T) : BNPairBoundedPredicate bp (setMul S T)

Product of BN-pair bounded sets is BN-pair bounded (uses finiteness of Bruhat cell products).

theorem CompactSubgroups.bnpair_inv_bounded {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (S : Set G) (hS : BNPairBoundedPredicate bp S) : BNPairBoundedPredicate bp ((fun (x : G) => x⁻¹) '' S)

The inverse of a BN-pair bounded set is BN-pair bounded.

theorem CompactSubgroups.bnpair_element_in_cell {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (g : G) : ∃ (w : M.Group), g ∈ bp.bruhatCell w

Every element of $G$ lies in some Bruhat cell of the BN-pair.

theorem CompactSubgroups.bnpair_union_bounded {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (S T : Set G) (hS : BNPairBoundedPredicate bp S) (hT : BNPairBoundedPredicate bp T) : BNPairBoundedPredicate bp (S ∪ T)

Union of two BN-pair bounded sets is BN-pair bounded.

theorem CompactSubgroups.proper_parabolic_finite {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (s : B_idx) : ∃ (ws : Finset M.Group), ∀ w ∈ bp.parabolicSubgroupW (Set.univ \ {s}), w ∈ ws

A proper coatom-type parabolic subgroup $\mathrm{Univ} \setminus \{s\}$ corresponds to a finite Weyl-image.

theorem CompactSubgroups.coatom_parabolic_bounded {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (s : B_idx) : BNPairBoundedPredicate bp (bp.standardParabolic (Set.univ \ {s}))

Each coatom standard parabolic subgroup $P_{\mathrm{Univ} \setminus \{s\}}$ is BN-pair bounded.

theorem CompactSubgroups.whole_group_not_bounded {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} [Infinite M.Group] (bp : BNPair G M) (bd : bp.BruhatProperties) : ¬BNPairBoundedPredicate bp (bp.standardParabolic Set.univ)

For infinite Weyl group, the whole group $G = P_{\mathrm{Univ}}$ is not BN-pair bounded.

theorem CompactSubgroups.standardParabolic_mono {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (S₁ S₂ : Set B_idx) (h : S₁ ⊆ S₂) : bp.standardParabolic S₁ ⊆ bp.standardParabolic S₂

Standard parabolic subgroups are monotone in the simple-root subset.

theorem CompactSubgroups.bruhatTitsFPT_maximal_is_coatom {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} [Infinite M.Group] (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (K : Subgroup G) (hK : IsMaximalBounded born K) (hB_le_K : bp.B ≤ K) (S' : Set B_idx) (hS' : ↑K = bp.standardParabolic S') : ∃ (s₀ : B_idx), S' = Set.univ \ {s₀}

Bruhat–Tits fixed point theorem (FPT) coatom step: if $K$ is a maximal bounded subgroup containing $B$ with $K = P_{S'}$, then $S'$ is a coatom $\mathrm{Univ} \setminus \{s_0\}$.

theorem CompactSubgroups.bruhatTitsFPT_conjugate_contains_B_geometric {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (K : Subgroup G) (hK : IsMaximalBounded born K) : ∃ (g : G), bp.B ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) K

Geometric input to Bruhat–Tits FPT: every maximal bounded subgroup $K$ admits a conjugate containing $B$.

theorem CompactSubgroups.subgroup_map_conj_carrier_subset_setMul {G : Type u_3} [Group G] (g : G) (K : Subgroup G) : ↑(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) K) ⊆ setMul (setMul {g} ↑K) {g⁻¹}

Carrier of a conjugated subgroup $gKg^{-1}$ lies inside the set product $\{g\} \cdot K \cdot \{g^{-1}\}$.

theorem CompactSubgroups.isBoundedSubgroup_map_conj {G : Type u_3} [Group G] (born : GroupBornology G) (K : Subgroup G) (hK : IsBoundedSubgroup born K) (g : G) : IsBoundedSubgroup born (Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) K)

Conjugation preserves boundedness of subgroups.

theorem CompactSubgroups.isMaximalBounded_map_conj {G : Type u_3} [Group G] (born : GroupBornology G) (K : Subgroup G) (hK : IsMaximalBounded born K) (g : G) : IsMaximalBounded born (Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) K)

Conjugation preserves maximal-boundedness of subgroups.

theorem CompactSubgroups.bruhatTitsFPT_conjugate_contains_B {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (K : Subgroup G) (hK : IsMaximalBounded born K) : ∃ (g : G), bp.B ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) K ∧ IsMaximalBounded born (Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) K)

Strengthened Bruhat–Tits FPT: a conjugate of a maximal bounded $K$ both contains $B$ and is itself maximal bounded.

theorem CompactSubgroups.subgroup_map_conj_coe {G : Type u_3} [Group G] (g : G) (K : Subgroup G) : ↑(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) K) = (fun (x : G) => g * x * g⁻¹) '' ↑K

Carrier set of $gKg^{-1}$ equals the conjugate image $\{gkg^{-1} : k \in K\}$.

theorem CompactSubgroups.bruhatTitsFPT_maximal_conjugate_to_standard {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} [Infinite M.Group] (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (K : Subgroup G) (hK : IsMaximalBounded born K) : ∃ (g : G) (s₀ : B_idx), (fun (x : G) => g * x * g⁻¹) '' ↑K = bp.standardParabolic (Set.univ \ {s₀})

Bruhat–Tits FPT: every maximal bounded subgroup $K$ is conjugate to a standard parabolic $P_{\mathrm{Univ} \setminus \{s_0\}}$.

theorem CompactSubgroups.bruhatTitsFPT_bounded_conj_in_proper_parabolic {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (K : Subgroup G) (hK : IsBoundedSubgroup born K) : ∃ (g : G) (S' : Set B_idx), S' ≠ Set.univ ∧ (fun (x : G) => g * x * g⁻¹) '' ↑K ⊆ bp.standardParabolic S'

Every bounded subgroup is contained, after conjugation, in some proper parabolic subgroup.

theorem CompactSubgroups.bruhatTitsFPT_bounded_conj_in_parabolic {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (K : Subgroup G) (hK : IsBoundedSubgroup born K) : ∃ (g : G) (s₀ : B_idx), (fun (x : G) => g * x * g⁻¹) '' ↑K ⊆ bp.standardParabolic (Set.univ \ {s₀})

Every bounded subgroup is contained, after conjugation, in some coatom standard parabolic $P_{\mathrm{Univ} \setminus \{s_0\}}$.

theorem CompactSubgroups.standardParabolic_order_reflects {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (S₁ S₂ : Set B_idx) : bp.standardParabolic S₁ ⊆ bp.standardParabolic S₂ → S₁ ⊆ S₂

The standard parabolic correspondence reflects the order: $P_{S_1} \subseteq P_{S_2}$ implies $S_1 \subseteq S_2$.

theorem CompactSubgroups.vertex_stabilizer_conj_is_maximal_bounded {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} [Infinite M.Group] (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (g : G) (s₀ : B_idx) (P_vs : Subgroup G) (hP_vs : ↑P_vs = bp.standardParabolic (Set.univ \ {s₀})) : IsMaximalBounded born (Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) P_vs)

A conjugate of a vertex stabilizer (coatom parabolic subgroup) is maximal bounded.

theorem CompactSubgroups.bruhatTitsFPT_bounded_has_maximal {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} [Infinite M.Group] (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (K : Subgroup G) (hK : IsBoundedSubgroup born K) : ∃ (K_max : Subgroup G), IsMaximalBounded born K_max ∧ K ≤ K_max

Every bounded subgroup is contained in some maximal bounded subgroup.

theorem CompactSubgroups.bruhatTitsFPT_geometric_core {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} [Infinite M.Group] (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (K : Subgroup G) (hK : IsBoundedSubgroup born K) : ∃ (g : G) (s₀ : B_idx) (K_max : Subgroup G), (fun (x : G) => g * x * g⁻¹) '' ↑K ⊆ bp.standardParabolic (Set.univ \ {s₀}) ∧ IsMaximalBounded born K_max ∧ K ≤ K_max

Combined geometric statement of Bruhat–Tits FPT: existence of conjugating $g$, vertex $s_0$, maximal bounded $K_{\max}$ containing $K$, with conjugated $K$ inside the coatom parabolic.

theorem CompactSubgroups.bruhatTitsFPT_bounded_in_maximal {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} [Infinite M.Group] (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (K : Subgroup G) (hK : IsBoundedSubgroup born K) : ∃ (K_max : Subgroup G), IsMaximalBounded born K_max ∧ K ≤ K_max

Wrapper: every bounded subgroup sits in some maximal bounded subgroup.

theorem CompactSubgroups.bruhatTitsFPT_bounded_in_vertex_stabilizer {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} [Infinite M.Group] (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (K : Subgroup G) (hK : IsBoundedSubgroup born K) : ∃ (g : G) (s₀ : B_idx), (fun (x : G) => g * x * g⁻¹) '' ↑K ⊆ bp.standardParabolic (Set.univ \ {s₀})

Every bounded subgroup is contained, up to conjugation, in a vertex stabilizer parabolic.

theorem CompactSubgroups.bounded_subgroup_in_maximal_bounded {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} [Infinite M.Group] (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (K : Subgroup G) (hK : IsBoundedSubgroup born K) : ∃ (K_max : Subgroup G), IsMaximalBounded born K_max ∧ K ≤ K_max

Alias: every bounded subgroup is contained in some maximal bounded subgroup.

theorem CompactSubgroups.maximal_bounded_eq_vertex_stabilizer {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} [Infinite M.Group] (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (K : Subgroup G) (hK : IsMaximalBounded born K) (hB_le_K : bp.B ≤ K) : ∃ (s₀ : B_idx), ↑K = bp.standardParabolic (Set.univ \ {s₀})

A maximal bounded subgroup containing $B$ equals a vertex-stabilizer parabolic $P_{\mathrm{Univ} \setminus \{s_0\}}$ for some $s_0$.

theorem CompactSubgroups.standardParabolic_maximal_bounded {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (s₀ : B_idx) (h_fin_parabolic : ∃ (ws : Finset M.Group), ∀ w ∈ bp.parabolicSubgroupW (Set.univ \ {s₀}), w ∈ ws) (h_not_bounded_top : ¬BNPairBoundedPredicate bp (bp.standardParabolic Set.univ)) (h_parabolic_reflects_order : ∀ (S₁ S₂ : Set B_idx), bp.standardParabolic S₁ ⊆ bp.standardParabolic S₂ → S₁ ⊆ S₂) : ∃ (K : Subgroup G), ↑K = bp.standardParabolic (Set.univ \ {s₀}) ∧ IsMaximalBounded born K ∧ bp.B ≤ K

Each coatom standard parabolic $P_{\mathrm{Univ} \setminus \{s_0\}}$ is a maximal bounded subgroup containing $B$.

theorem CompactSubgroups.bounded_subgroup_in_vertex_stabilizer {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} [Infinite M.Group] (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (K : Subgroup G) (hK : IsBoundedSubgroup born K) : ∃ (g : G) (s₀ : B_idx), (fun (x : G) => g * x * g⁻¹) '' ↑K ⊆ bp.standardParabolic (Set.univ \ {s₀})

Alias: every bounded subgroup is conjugate-contained in a vertex-stabilizer parabolic.

theorem CompactSubgroups.maximal_bounded_conjugate_to_standard {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} [Infinite M.Group] (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (K : Subgroup G) (hK : IsMaximalBounded born K) : ∃ (g : G) (s₀ : B_idx), (fun (x : G) => g * x * g⁻¹) '' ↑K = bp.standardParabolic (Set.univ \ {s₀})

Alias: every maximal bounded subgroup is conjugate to a standard coatom parabolic.

theorem CompactSubgroups.BNPairBoundedness {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} [Infinite M.Group] (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (h_fin_parabolic : ∀ (s₀ : B_idx), ∃ (ws : Finset M.Group), ∀ w ∈ bp.parabolicSubgroupW (Set.univ \ {s₀}), w ∈ ws) (h_not_bounded_top : ¬BNPairBoundedPredicate bp (bp.standardParabolic Set.univ)) (h_parabolic_reflects_order : ∀ (S₁ S₂ : Set B_idx), bp.standardParabolic S₁ ⊆ bp.standardParabolic S₂ → S₁ ⊆ S₂) : (∀ (K : Subgroup G), IsBoundedSubgroup born K → ∃ (K_max : Subgroup G), IsMaximalBounded born K_max ∧ K ≤ K_max) ∧ (∀ (K : Subgroup G), IsBoundedSubgroup born K → ∃ (g : G) (s₀ : B_idx), (fun (x : G) => g * x * g⁻¹) '' ↑K ⊆ bp.standardParabolic (Set.univ \ {s₀})) ∧ (∀ (K : Subgroup G), IsMaximalBounded born K → bp.B ≤ K → ∃ (s₀ : B_idx), ↑K = bp.standardParabolic (Set.univ \ {s₀})) ∧ (∀ (s₀ : B_idx), ∃ (K : Subgroup G), ↑K = bp.standardParabolic (Set.univ \ {s₀}) ∧ IsMaximalBounded born K ∧ bp.B ≤ K) ∧ ∀ (K : Subgroup G), IsMaximalBounded born K → ∃ (g : G) (s₀ : B_idx), (fun (x : G) => g * x * g⁻¹) '' ↑K = bp.standardParabolic (Set.univ \ {s₀})

Main BN-pair boundedness theorem (Section 17.7): a five-part conjunction packaging the various parts of the Bruhat–Tits fixed point theorem under the relevant finiteness hypotheses.

structure CompactSubgroups.IsSpecialVertex {B_idx : Type u_2} (M : CoxeterMatrix B_idx) (linearPart : M.Group →* M.Group) (s₀ : B_idx) : Prop

$s_0$ is a special vertex (with respect to a linear-part homomorphism) if every element in the image of the linear part has a preimage in the standard parabolic $W_{\mathrm{Univ} \setminus \{s_0\}}$.

• surjective (wbar : M.Group) : wbar ∈ Set.range ⇑linearPart → ∃ w ∈ ↑(Subgroup.closure (M.toCoxeterSystem.simple '' (Set.univ \ {s₀}))), linearPart w = wbar

structure CompactSubgroups.GoodMaximalBounded {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (born : GroupBornology G) (linearPart : M.Group →* M.Group) : Type (max u_1 u_2)

A good maximal bounded subgroup: a maximal bounded subgroup $K$ containing $B$ that equals a coatom standard parabolic $P_{\mathrm{Univ} \setminus \{\mathrm{vertex}\}}$ where the vertex is special.

• K : Subgroup G
• maximal_bounded : IsMaximalBounded born self.K
• contains_B : bp.B ≤ self.K
• vertex : B_idx
• eq_parabolic : ↑self.K = bp.standardParabolic (Set.univ \ {self.vertex})
• is_special : IsSpecialVertex M linearPart self.vertex

theorem CompactSubgroups.good_maximal_bounded_exists {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (linearPart : M.Group →* M.Group) (hM_indec : M.IsIndecomposable) (hM_aff : M.IsAffine) (h_special : ∃ (s₀ : B_idx), IsSpecialVertex M linearPart s₀) (h_fin_parabolic : ∀ (s₀ : B_idx), ∃ (ws : Finset M.Group), ∀ w ∈ bp.parabolicSubgroupW (Set.univ \ {s₀}), w ∈ ws) (h_not_bounded_top : ¬BNPairBoundedPredicate bp (bp.standardParabolic Set.univ)) (h_parabolic_reflects_order : ∀ (S₁ S₂ : Set B_idx), bp.standardParabolic S₁ ⊆ bp.standardParabolic S₂ → S₁ ⊆ S₂) : ∃ (s₀ : B_idx) (K : Subgroup G), ↑K = bp.standardParabolic (Set.univ \ {s₀}) ∧ IsMaximalBounded born K ∧ bp.B ≤ K ∧ IsSpecialVertex M linearPart s₀

For an indecomposable affine Coxeter matrix admitting a special vertex, there exists a good maximal bounded subgroup.

theorem CompactSubgroups.standardParabolic_maximal_bounded' {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} [Infinite M.Group] (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (s₀ : B_idx) (h_parabolic_reflects_order : ∀ (S₁ S₂ : Set B_idx), bp.standardParabolic S₁ ⊆ bp.standardParabolic S₂ → S₁ ⊆ S₂) : ∃ (K : Subgroup G), ↑K = bp.standardParabolic (Set.univ \ {s₀}) ∧ IsMaximalBounded born K ∧ bp.B ≤ K

Specialization of standardParabolic_maximal_bounded for infinite Weyl groups, using proper_parabolic_finite and whole_group_not_bounded as the finiteness inputs.

theorem CompactSubgroups.BNPairBoundedness' {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} [Infinite M.Group] (bp : BNPair G M) (bd : bp.BruhatProperties) (born : GroupBornology G) (hborn : born.isBounded = BNPairBoundedPredicate bp) (h_parabolic_reflects_order : ∀ (S₁ S₂ : Set B_idx), bp.standardParabolic S₁ ⊆ bp.standardParabolic S₂ → S₁ ⊆ S₂) : (∀ (K : Subgroup G), IsBoundedSubgroup born K → ∃ (K_max : Subgroup G), IsMaximalBounded born K_max ∧ K ≤ K_max) ∧ (∀ (K : Subgroup G), IsBoundedSubgroup born K → ∃ (g : G) (s₀ : B_idx), (fun (x : G) => g * x * g⁻¹) '' ↑K ⊆ bp.standardParabolic (Set.univ \ {s₀})) ∧ (∀ (K : Subgroup G), IsMaximalBounded born K → bp.B ≤ K → ∃ (s₀ : B_idx), ↑K = bp.standardParabolic (Set.univ \ {s₀})) ∧ (∀ (s₀ : B_idx), ∃ (K : Subgroup G), ↑K = bp.standardParabolic (Set.univ \ {s₀}) ∧ IsMaximalBounded born K ∧ bp.B ≤ K) ∧ ∀ (K : Subgroup G), IsMaximalBounded born K → ∃ (g : G) (s₀ : B_idx), (fun (x : G) => g * x * g⁻¹) '' ↑K = bp.standardParabolic (Set.univ \ {s₀})

Specialization of BNPairBoundedness to infinite Weyl groups assuming only the order-reflection hypothesis.