Bruhat functions

TheoremOrbit-normalized weights give equal nonnegative integrals#✓fully proved

Nonnegative integrals of an invariant function agree for orbit-normalized weights. Normalization is needed only where the function is nonzero, and the common integral is allowed to be infinite.

theorem lintegral_mul_eq_of_normalized_smul
    (hact : Measurable fun p : A × X => p.1 • p.2)
    (hμ : ∀ a : A, MeasurePreserving (fun x : X => a • x) μ μ)
    {f w₁ w₂ : X → ℝ≥0∞} (hf : Measurable f)
    (hfinv : ∀ (a : A) (x : X), f (a • x) = f x)
    (hw₁ : Measurable w₁) (hw₂ : Measurable w₂)
    (h₁ : ∀ x, f x ≠ 0 → ∫⁻ a, w₁ (a • x) ∂τ = 1)
    (h₂ : ∀ x, f x ≠ 0 → ∫⁻ a, w₂ (a • x) ∂τ = 1) :
    ∫⁻ x, f x * w₁ x ∂μ = ∫⁻ x, f x * w₂ x ∂μ

Used by 2

Used byIntegrability is independent of the orbit-normalized weight · Orbit-normalized cutoffs give equal complex integrals

TheoremIntegrability is independent of the orbit-normalized weight#✓fully proved

Integrability of an invariant complex function times a nonnegative real weight is independent of the weight when both orbit averages are one on the function's support. Neither weighted function is required to be integrable.

theorem integrable_mul_iff_of_normalized_smul
    (hact : Measurable fun p : A × X => p.1 • p.2)
    (hμ : ∀ a : A, MeasurePreserving (fun x : X => a • x) μ μ)
    (hf : Measurable f) (hfinv : ∀ (a : A) (x : X), f (a • x) = f x)
    (hw₁ : Measurable w₁) (hw₂ : Measurable w₂)
    (hw₁0 : ∀ x, 0 ≤ w₁ x) (hw₂0 : ∀ x, 0 ≤ w₂ x)
    (h₁ : ∀ x, f x ≠ 0 → ∫⁻ a, ENNReal.ofReal (w₁ (a • x)) ∂τ = 1)
    (h₂ : ∀ x, f x ≠ 0 → ∫⁻ a, ENNReal.ofReal (w₂ (a • x)) ∂τ = 1) :
    Integrable (fun x => f x * (w₁ x : ℂ)) μ ↔
      Integrable (fun x => f x * (w₂ x : ℂ)) μ

Uses 1 · Used by 1

Proof usesOrbit-normalized weights give equal nonnegative integrals

Used byOrbit-normalized cutoffs give equal complex integrals

TheoremOrbit-normalized cutoffs give equal complex integrals#✓fully proved

Weighted integrals of an invariant complex function agree for nonnegative orbit-normalized cutoffs. If one weighted function is not integrable, neither is the other, and both Bochner integrals are zero.

theorem integral_mul_eq_of_normalized_smul
    (hact : Measurable fun p : A × X => p.1 • p.2)
    (hμ : ∀ a : A, MeasurePreserving (fun x : X => a • x) μ μ)
    (hf : Measurable f) (hfinv : ∀ (a : A) (x : X), f (a • x) = f x)
    (hw₁ : Measurable w₁) (hw₂ : Measurable w₂)
    (hw₁0 : ∀ x, 0 ≤ w₁ x) (hw₂0 : ∀ x, 0 ≤ w₂ x)
    (h₁ : ∀ x, f x ≠ 0 → ∫⁻ a, ENNReal.ofReal (w₁ (a • x)) ∂τ = 1)
    (h₂ : ∀ x, f x ≠ 0 → ∫⁻ a, ENNReal.ofReal (w₂ (a • x)) ∂τ = 1) :
    ∫ x, f x * (w₁ x : ℂ) ∂μ = ∫ x, f x * (w₂ x : ℂ) ∂μ

Uses 2 · Used by 1

Proof usesIntegrability is independent of the orbit-normalized weight · Orbit-normalized weights give equal nonnegative integrals

Used bySubgroup-normalized weights give equal integrals

TheoremSubgroup-normalized weights give equal integrals#✓fully proved

Subgroup-normalized nonnegative weights give the same integral of an invariant complex function. This measure-theoretic statement requires neither a closed subgroup nor compact supports nor a bounded function.

theorem integral_mul_eq_of_normalized_subgroup
    {G : Type*} [Group G] [MeasurableSpace G] [MeasurableMul₂ G]
    (μ : Measure G) [SFinite μ] [μ.IsMulLeftInvariant]
    (T : Subgroup G) [MeasurableSpace T] [MeasurableInv T]
    (hT : Measurable (Subtype.val : T → G))
    (τ : Measure T) [SFinite τ] [τ.IsInvInvariant]
    (f : G → ℂ) (hf : Measurable f)
    (hfinv : ∀ (t : T) (x : G), f ((t : G) * x) = f x)
    (w₁ w₂ : G → ℝ) (hw₁0 : ∀ x, 0 ≤ w₁ x) (hw₂0 : ∀ x, 0 ≤ w₂ x)
    (hw₁ : Measurable w₁) (hw₂ : Measurable w₂)
    (h₁ : ∀ x, f x ≠ 0 → ∫ t : T, w₁ ((t : G) * x) ∂τ = 1)
    (h₂ : ∀ x, f x ≠ 0 → ∫ t : T, w₂ ((t : G) * x) ∂τ = 1) :
    ∫ x, f x * (w₁ x : ℂ) ∂μ = ∫ x, f x * (w₂ x : ℂ) ∂μ

Uses 1 · Used by 1

Proof usesOrbit-normalized cutoffs give equal complex integrals

Used byCutoff independence of integrals of bounded invariant functions

TheoremContinuous cutoff for a closed-embedding homomorphism#✓fully proved

A continuous nonnegative compactly supported cutoff normalized on every left orbit meeting K, for a closed-embedding homomorphism ι. The measure may have any scale. No Hausdorff or countability hypotheses are required.

theorem exists_continuous_cutoff_of_isClosedEmbedding
    [τ.IsOpenPosMeasure] [τ.IsMulRightInvariant]
    (K : Set G) (hK : IsCompact K) :
    ∃ w : G → ℝ, Continuous w ∧ HasCompactSupport w ∧ (∀ x, 0 ≤ w x) ∧
      ∀ (h : H) (k : G), k ∈ K → ∫ h', w (ι h' * (ι h * k)) ∂τ = 1

Used by 1

Used byContinuous Bruhat cutoff for a closed subgroup

TheoremContinuous Bruhat cutoff for a closed subgroup#✓fully proved

A continuous nonnegative compactly supported Bruhat cutoff for a closed subgroup, normalized on any subset of the saturation of a compact set.

theorem exists_continuous_cutoff_of_subset_mul
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [LocallyCompactSpace G] (T : Subgroup G) (hT : IsClosed (T : Set G))
    [MeasurableSpace T] [BorelSpace T] (τ : Measure T)
    [IsFiniteMeasureOnCompacts τ] [τ.IsOpenPosMeasure] [τ.IsMulRightInvariant]
    {E K : Set G} (hK : IsCompact K) (hE : E ⊆ (T : Set G) * K) :
    ∃ w : G → ℝ, Continuous w ∧ HasCompactSupport w ∧ (∀ x, 0 ≤ w x) ∧
      ∀ x ∈ E, ∫ t : T, w ((t : G) * x) ∂τ = 1

Uses 1 · Used by 2

Proof usesContinuous cutoff for a closed-embedding homomorphism

Used byExistence of a Bruhat section for a closed subgroup · Positive common integral of cocompact subgroup cutoffs

TheoremExistence of a Bruhat section for a closed subgroup#✓fully proved

A Bruhat section: given a closed subgroup T of a locally compact group and a set E contained in T * C for compact C, there is a compactly supported nonnegative measurable function w whose integral over each T-translate meeting E equals 1.

Use exists_continuous_cutoff_of_subset_mul when continuity or boundedness is needed. These functions normalize subgroup integrals; they are not sections of the quotient map.

theorem exists_hasCompactSupport_integral_subgroup_translate_eq_one_of_subset_mul
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [LocallyCompactSpace G] [SecondCountableTopology G] [MeasurableSpace G]
    [BorelSpace G] (T : Subgroup G) (hT : IsClosed (T : Set G))
    [MeasurableSpace T] [BorelSpace T] (τ : Measure T) [τ.IsHaarMeasure]
    [τ.IsMulRightInvariant] {E C : Set G} (hC : IsCompact C)
    (hE : E ⊆ (T : Set G) * C) :
    ∃ w : G → ℝ, (∀ x, 0 ≤ w x) ∧ Measurable w ∧ HasCompactSupport w ∧
      ∀ x ∈ E, ∫ t : T, w ((t : G) * x) ∂τ = 1

Uses 1

Proof usesContinuous Bruhat cutoff for a closed subgroup

TheoremBounded invariant functions are integrable against normalized cutoffs#✓fully proved

A bounded measurable T-invariant complex function is integrable against any nonnegative measurable compactly supported weight whose T-average is one wherever the function is nonzero. The weight need not be bounded.

theorem integrable_mul_of_integral_subgroup_translate_eq_one
    (F : G → ℂ) (hFm : Measurable F) (hFb : ∃ C : ℝ, ∀ x, ‖F x‖ ≤ C)
    (hFT : ∀ (t : T) (x : G), F ((t : G) * x) = F x)
    (w : G → ℝ) (hw0 : ∀ x, 0 ≤ w x) (hwm : Measurable w)
    (hwc : HasCompactSupport w)
    (hw1 : ∀ x, F x ≠ 0 → ∫ t : T, w ((t : G) * x) ∂τ = 1) :
    Integrable (fun x => F x * (w x : ℂ)) μ

Used by 1

Used byPositive common integral of cocompact subgroup cutoffs

TheoremCutoff independence of integrals of bounded invariant functions#✓fully proved

The integral of a bounded measurable T-invariant complex function against a nonnegative measurable compactly supported cutoff does not depend on the cutoff, when each cutoff has subgroup integral one on the support of that function. Normalization is not required outside its support.

The more general integral_mul_eq_of_normalized_subgroup does not require boundedness or compact support; the hypotheses here also guarantee integrability by integrable_mul_of_integral_subgroup_translate_eq_one.

theorem integral_mul_eq_integral_mul_of_integral_subgroup_translate_eq_one
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G]
    [SecondCountableTopology G] [MeasurableSpace G] [BorelSpace G]
    (T : Subgroup G) (hT : IsClosed (T : Set G)) [MeasurableSpace T] [BorelSpace T]
    (μ : Measure G) [μ.IsHaarMeasure] (τ : Measure T) [τ.IsHaarMeasure] [τ.IsInvInvariant]
    (F : G → ℂ) (hFm : Measurable F) (hFb : ∃ C : ℝ, ∀ x, ‖F x‖ ≤ C)
    (hFT : ∀ (t : T) (x : G), F ((t : G) * x) = F x)
    (w₁ w₂ : G → ℝ)
    (hw₁ : (∀ x, 0 ≤ w₁ x) ∧ Measurable w₁ ∧ HasCompactSupport w₁ ∧
      ∀ x, F x ≠ 0 → ∫ t : T, w₁ ((t : G) * x) ∂τ = 1)
    (hw₂ : (∀ x, 0 ≤ w₂ x) ∧ Measurable w₂ ∧ HasCompactSupport w₂ ∧
      ∀ x, F x ≠ 0 → ∫ t : T, w₂ ((t : G) * x) ∂τ = 1) :
    ∫ x, F x * (w₁ x : ℂ) ∂μ = ∫ x, F x * (w₂ x : ℂ) ∂μ

Uses 1 · Used by 1

Proof usesSubgroup-normalized weights give equal integrals

Used byPositive common integral of cocompact subgroup cutoffs

TheoremPositive common integral of cocompact subgroup cutoffs#✓fully proved

A compact cocompactness witness gives a continuous normalized cutoff and a positive common integral for all nonnegative measurable compactly supported normalized cutoffs. Every such cutoff is genuinely integrable, even when it is not bounded. Neither the ambient group nor the subgroup must be Hausdorff.

MeasureTheory.exists_pos_integral_cutoff_of_cocompact · 16 lines

theorem exists_pos_integral_cutoff_of_cocompact
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [LocallyCompactSpace G] [SecondCountableTopology G]
    [MeasurableSpace G] [BorelSpace G]
    (T : Subgroup G) (hT : IsClosed (T : Set G))
    [MeasurableSpace T] [BorelSpace T]
    (μ : Measure G) [μ.IsHaarMeasure] (τ : Measure T)
    [τ.IsHaarMeasure] [τ.IsInvInvariant]
    (K : Set G) (hK : IsCompact K)
    (hcov : ∀ x : G, ∃ t : T, ∃ k ∈ K, x = (t : G) * k) :
    ∃ κ : ℝ, 0 < κ ∧
      (∃ w : G → ℝ, (∀ x, 0 ≤ w x) ∧ Continuous w ∧ HasCompactSupport w ∧
        ∀ x, ∫ t : T, w ((t : G) * x) ∂τ = 1) ∧
      ∀ w : G → ℝ, (∀ x, 0 ≤ w x) → Measurable w → HasCompactSupport w →
        (∀ x, ∫ t : T, w ((t : G) * x) ∂τ = 1) →
        Integrable w μ ∧ ∫ x, w x ∂μ = κ

Uses 3

Proof usesContinuous Bruhat cutoff for a closed subgroup · Bounded invariant functions are integrable against normalized cutoffs · Cutoff independence of integrals of bounded invariant functions

TheoremExistence of a locally constant normalized subgroup cutoff#✓fully proved

A compact set in a topological group with a compact open subgroup has a nonnegative locally constant cutoff whose integral over every left T-orbit meeting that set is one, for a closed commutative subgroup T. The same compactly supported function works simultaneously on all of T * Ω. The Haar measure need not have any prescribed normalization.

theorem exists_isLocallyConstant_integral_subgroup_mul_eq_one
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (K : Subgroup G) (hK : IsCompact (K : Set G))
    (hK' : IsOpen (K : Set G))
    (T : Subgroup G) (hT : IsClosed (T : Set G))
    (hcomm : ∀ s ∈ T, ∀ t ∈ T, s * t = t * s)
    [MeasurableSpace T] [BorelSpace T] (τ : Measure T) [τ.IsHaarMeasure]
    (Ω : Set G) (hΩ : IsCompact Ω) :
    ∃ w : G → ℝ, (∀ x, 0 ≤ w x) ∧ IsLocallyConstant w ∧
      HasCompactSupport w ∧ ∀ x : G,
      (∃ t ∈ T, ∃ d ∈ Ω, x = t * d) → ∫ t : T, w (t * x) ∂τ = 1

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.