ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>self : Besicovitch.BallPackage β α<VAR>b : β<GOAL>0 < self.r b
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>self : Besicovitch.BallPackage β α<VAR>b : β<GOAL>self.r b ≤ self.r_bound
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>self : Besicovitch.TauPackage β α<GOAL>1 < self.τ
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>β : Type u<VAR>Nonempty β<VAR>p : Besicovitch.TauPackage β α<GOAL>Monotone p.iUnionUpTo
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>β : Type u<VAR>Nonempty β<VAR>p : Besicovitch.TauPackage β α<GOAL>{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>β : Type u<VAR>Nonempty β<VAR>p : Besicovitch.TauPackage β α<VAR>x : β<GOAL>p.c x ∈ p.iUnionUpTo p.lastStep
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>β : Type u<VAR>Nonempty β<VAR>p : Besicovitch.TauPackage β α<VAR>i : Ordinal.{u}<VAR>hi : i < p.lastStep<VAR>N : ℕ<VAR>hN : IsEmpty (Besicovitch.SatelliteConfig α N p.τ)<GOAL>p.color i < N
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>β : Type u<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (Besicovitch.SatelliteConfig α N τ)<VAR>q : Besicovitch.BallPackage β α<GOAL>∃ s, (∀ (i : Fin N), (s i).PairwiseDisjoint fun j => Metric.closedBall (q.c j) (q.r j)) ∧ Set.range q.c ⊆ ⋃ i, ⋃ j ∈ s i, Metric.ball (q.c j) (q.r j)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>SecondCountableTopology α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (Besicovitch.SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, Metric.closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => Metric.closedBall x (r x)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>SecondCountableTopology α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>HasBesicovitchCovering α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty<GOAL>∃ t, t.Countable ∧ (∀ p ∈ t, p.1 ∈ s) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, Metric.closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun p => Metric.closedBall p.1 p.2
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>SecondCountableTopology α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>HasBesicovitchCovering α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty<GOAL>∃ t, t.Countable ∧ (∀ p ∈ t, p.1 ∈ s) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, Metric.closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun p => Metric.closedBall p.1 p.2
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>SecondCountableTopology α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>HasBesicovitchCovering α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty<VAR>R : α → ℝ<VAR>hR : ∀ x ∈ s, 0 < R x<GOAL>∃ t r, t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x ∩ Set.Ioo 0 (R x)) ∧ μ (s \ ⋃ x ∈ t, Metric.closedBall x (r x)) = 0 ∧ t.PairwiseDisjoint fun x => Metric.closedBall x (r x)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>SecondCountableTopology α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>HasBesicovitchCovering α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>μ.OuterRegular<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty<GOAL>∃ t r, t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x) ∧ s ⊆ ⋃ x ∈ t, Metric.closedBall x (r x) ∧ ∑' (x : ↑t), μ (Metric.closedBall (↑x) (r ↑x)) ≤ μ s + ε
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>SecondCountableTopology α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>HasBesicovitchCovering α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>x : α<GOAL>Filter.Tendsto (fun r => Metric.closedBall x r) (𝓝[>] 0) ((Besicovitch.vitaliFamily μ).filterAt x)
<VAR>β : Type u<VAR>MetricSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>SecondCountableTopology β<VAR>HasBesicovitchCovering β<VAR>ρ μ : MeasureTheory.Measure β<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<GOAL>∀ᵐ (x : β) ∂μ, Filter.Tendsto (fun r => ρ (Metric.closedBall x r) / μ (Metric.closedBall x r)) (𝓝[>] 0) (𝓝 (ρ.rnDeriv μ x))
<VAR>β : Type u<VAR>MetricSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>SecondCountableTopology β<VAR>HasBesicovitchCovering β<VAR>μ : MeasureTheory.Measure β<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : β) ∂μ, Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (𝓝[>] 0) (𝓝 (s.indicator 1 x))
<VAR>β : Type u<VAR>MetricSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>SecondCountableTopology β<VAR>HasBesicovitchCovering β<VAR>μ : MeasureTheory.Measure β<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>s : Set β<GOAL>∀ᵐ (x : β) ∂μ.restrict s, Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (𝓝[>] 0) (𝓝 1)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : ¬MeasureTheory.Integrable (fun x => rexp (f x)) μ<GOAL>μ.tilted f = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : ¬AEMeasurable f μ<GOAL>μ.tilted f = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>f : α → ℝ<GOAL>MeasureTheory.Measure.tilted 0 f = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>c : ℝ<GOAL>(μ.tilted fun x => c) = (μ Set.univ)⁻¹ • μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>c : ℝ<GOAL>(μ.tilted fun x => c) = μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.tilted 0 = (μ Set.univ)⁻¹ • μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>μ.tilted 0 = μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>hfg : f =ᵐ[μ] g<GOAL>μ.tilted f = μ.tilted g
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<GOAL>μ.tilted f = μ.withDensity fun x => ↑⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.tilted f) s = ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>f : α → ℝ<VAR>s : Set α<GOAL>(μ.tilted f) s = ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ<VAR>hs : MeasurableSet s<GOAL>(μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>f : α → ℝ<VAR>s : Set α<GOAL>(μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>NeZero μ<VAR>hf : MeasureTheory.Integrable (fun x => rexp (f x)) μ<GOAL>MeasureTheory.IsProbabilityMeasure (μ.tilted f)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>g : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>f : α → ℝ<VAR>g : α → ℝ≥0∞<VAR>s : Set α<GOAL>∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>g : α → ℝ≥0∞<GOAL>∫⁻ (x : α), g x ∂μ.tilted f = ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → ℝ<VAR>g : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f : α → ℝ<VAR>g : α → E<VAR>s : Set α<GOAL>∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → ℝ<VAR>g : α → E<GOAL>∫ (x : α), g x ∂μ.tilted f = ∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<GOAL>∫ (x : α), rexp (g x) ∂μ.tilted f = (∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable (fun x => rexp (f x)) μ<VAR>g : α → ℝ<GOAL>(μ.tilted f).tilted g = μ.tilted (f + g)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable (fun x => rexp (f x)) μ<VAR>g : α → ℝ<VAR>hg : MeasureTheory.Integrable (fun x => rexp (g x)) μ<GOAL>(μ.tilted f).tilted g = (μ.tilted g).tilted f
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable (fun x => rexp (f x)) μ<GOAL>(μ.tilted f).tilted (-f) = (μ Set.univ)⁻¹ • μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hf : MeasureTheory.Integrable (fun x => rexp (f x)) μ<GOAL>(μ.tilted f).tilted (-f) = μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<GOAL>(μ.tilted f).AbsolutelyContinuous μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable (fun x => rexp (f x)) μ<GOAL>μ.AbsolutelyContinuous (μ.tilted f)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hf : MeasureTheory.Integrable (fun x => rexp (f x)) ν<GOAL>μ.rnDeriv (ν.tilted f) =ᵐ[ν] fun x => ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hf : MeasureTheory.Integrable (fun x => rexp (f x)) ν<GOAL>(fun x => (μ.rnDeriv (ν.tilted f) x).toReal) =ᵐ[ν] fun x => (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hfν : AEMeasurable f ν<GOAL>(μ.tilted f).rnDeriv ν =ᵐ[ν] fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hfν : AEMeasurable f ν<GOAL>(fun x => ((μ.tilted f).rnDeriv ν x).toReal) =ᵐ[ν] fun x => (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.SigmaFinite μ<VAR>hf : AEMeasurable f μ<GOAL>(μ.tilted f).rnDeriv μ =ᵐ[μ] fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.SigmaFinite μ<VAR>hf : MeasureTheory.Integrable (fun x => rexp (f x)) μ<GOAL>(fun x => Real.log ((μ.tilted f).rnDeriv μ x).toReal) =ᵐ[μ] fun x => f x - Real.log (∫ (x : α), rexp (f x) ∂μ)
<VAR>G : Type u_1<VAR>Group G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>BorelSpace G<VAR>PolishSpace G<VAR>ν : MeasureTheory.Measure G<VAR>Γ : Subgroup G<VAR>T2Space (G ⧸ Γ)<VAR>SecondCountableTopology (G ⧸ Γ)<VAR>μ : MeasureTheory.Measure (G ⧸ Γ)<VAR>MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ<VAR>ν.IsMulLeftInvariant<VAR>hasFun : MeasureTheory.HasFundamentalDomain (↥Γ.op) G ν<GOAL>MeasureTheory.SMulInvariantMeasure G (G ⧸ Γ) μ
<VAR>G : Type u_1<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>PolishSpace G<VAR>ν : MeasureTheory.Measure G<VAR>Γ : AddSubgroup G<VAR>T2Space (G ⧸ Γ)<VAR>SecondCountableTopology (G ⧸ Γ)<VAR>μ : MeasureTheory.Measure (G ⧸ Γ)<VAR>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ<VAR>ν.IsAddLeftInvariant<VAR>hasFun : MeasureTheory.HasAddFundamentalDomain (↥Γ.op) G ν<GOAL>MeasureTheory.VAddInvariantMeasure G (G ⧸ Γ) μ
<VAR>G : Type u_1<VAR>Group G<VAR>MeasurableSpace G<VAR>ν : MeasureTheory.Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>μ : MeasureTheory.Measure (G ⧸ Γ)<VAR>MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ<GOAL>MeasureTheory.MeasurePreserving QuotientGroup.mk (ν.restrict 𝓕) μ
<VAR>G : Type u_1<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>ν : MeasureTheory.Measure G<VAR>Γ : AddSubgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>μ : MeasureTheory.Measure (G ⧸ Γ)<VAR>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ<GOAL>MeasureTheory.MeasurePreserving QuotientAddGroup.mk (ν.restrict 𝓕) μ
<VAR>G : Type u_1<VAR>Group G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>BorelSpace G<VAR>PolishSpace G<VAR>Γ : Subgroup G<VAR>Γ.Normal<VAR>T2Space (G ⧸ Γ)<VAR>SecondCountableTopology (G ⧸ Γ)<VAR>μ : MeasureTheory.Measure (G ⧸ Γ)<VAR>ν : MeasureTheory.Measure G<VAR>ν.IsMulLeftInvariant<VAR>hasFun : MeasureTheory.HasFundamentalDomain (↥Γ.op) G ν<VAR>MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ<GOAL>μ.IsMulLeftInvariant
<VAR>G : Type u_1<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>PolishSpace G<VAR>Γ : AddSubgroup G<VAR>Γ.Normal<VAR>T2Space (G ⧸ Γ)<VAR>SecondCountableTopology (G ⧸ Γ)<VAR>μ : MeasureTheory.Measure (G ⧸ Γ)<VAR>ν : MeasureTheory.Measure G<VAR>ν.IsAddLeftInvariant<VAR>hasFun : MeasureTheory.HasAddFundamentalDomain (↥Γ.op) G ν<VAR>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ<GOAL>μ.IsAddLeftInvariant
<VAR>G : Type u_1<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>PolishSpace G<VAR>Γ : AddSubgroup G<VAR>Countable ↥Γ<VAR>Γ.Normal<VAR>T2Space (G ⧸ Γ)<VAR>SecondCountableTopology (G ⧸ Γ)<VAR>μ : MeasureTheory.Measure (G ⧸ Γ)<VAR>ν : MeasureTheory.Measure G<VAR>ν.IsAddLeftInvariant<VAR>ν.IsAddRightInvariant<VAR>MeasureTheory.SigmaFinite ν<VAR>μ.IsAddLeftInvariant<VAR>MeasureTheory.SigmaFinite μ<VAR>s : Set G<VAR>fund_dom_s : MeasureTheory.IsAddFundamentalDomain (↥Γ.op) s ν<VAR>V : Set (G ⧸ Γ)<VAR>meas_V : MeasurableSet V<VAR>neZeroV : μ V ≠ 0<VAR>hV : μ V = ν (QuotientAddGroup.mk ⁻¹' V ∩ s)<VAR>neTopV : μ V ≠ ⊤<GOAL>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ
<VAR>G : Type u_1<VAR>Group G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>BorelSpace G<VAR>PolishSpace G<VAR>Γ : Subgroup G<VAR>Countable ↥Γ<VAR>Γ.Normal<VAR>T2Space (G ⧸ Γ)<VAR>SecondCountableTopology (G ⧸ Γ)<VAR>μ : MeasureTheory.Measure (G ⧸ Γ)<VAR>ν : MeasureTheory.Measure G<VAR>ν.IsMulLeftInvariant<VAR>ν.IsMulRightInvariant<VAR>MeasureTheory.SigmaFinite ν<VAR>μ.IsMulLeftInvariant<VAR>MeasureTheory.SigmaFinite μ<VAR>s : Set G<VAR>fund_dom_s : MeasureTheory.IsFundamentalDomain (↥Γ.op) s ν<VAR>V : Set (G ⧸ Γ)<VAR>meas_V : MeasurableSet V<VAR>neZeroV : μ V ≠ 0<VAR>hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)<VAR>neTopV : μ V ≠ ⊤<GOAL>MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ
<VAR>G : Type u_1<VAR>Group G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>BorelSpace G<VAR>PolishSpace G<VAR>Γ : Subgroup G<VAR>Countable ↥Γ<VAR>Γ.Normal<VAR>T2Space (G ⧸ Γ)<VAR>SecondCountableTopology (G ⧸ Γ)<VAR>μ : MeasureTheory.Measure (G ⧸ Γ)<VAR>ν : MeasureTheory.Measure G<VAR>ν.IsMulLeftInvariant<VAR>ν.IsMulRightInvariant<VAR>MeasureTheory.SigmaFinite ν<VAR>μ.IsMulLeftInvariant<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hasFun : MeasureTheory.HasFundamentalDomain (↥Γ.op) G ν<VAR>h : MeasureTheory.covolume (↥Γ.op) G ν = μ Set.univ<GOAL>MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ
<VAR>G : Type u_1<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>PolishSpace G<VAR>Γ : AddSubgroup G<VAR>Countable ↥Γ<VAR>Γ.Normal<VAR>T2Space (G ⧸ Γ)<VAR>SecondCountableTopology (G ⧸ Γ)<VAR>μ : MeasureTheory.Measure (G ⧸ Γ)<VAR>ν : MeasureTheory.Measure G<VAR>ν.IsAddLeftInvariant<VAR>ν.IsAddRightInvariant<VAR>MeasureTheory.SigmaFinite ν<VAR>μ.IsAddLeftInvariant<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hasFun : MeasureTheory.HasAddFundamentalDomain (↥Γ.op) G ν<VAR>h : MeasureTheory.addCovolume (↥Γ.op) G ν = μ Set.univ<GOAL>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ
<VAR>G : Type u_1<VAR>Group G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>BorelSpace G<VAR>PolishSpace G<VAR>Γ : Subgroup G<VAR>Countable ↥Γ<VAR>Γ.Normal<VAR>T2Space (G ⧸ Γ)<VAR>SecondCountableTopology (G ⧸ Γ)<VAR>μ : MeasureTheory.Measure (G ⧸ Γ)<VAR>ν : MeasureTheory.Measure G<VAR>ν.IsHaarMeasure<VAR>ν.IsMulRightInvariant<VAR>LocallyCompactSpace G<VAR>MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ<VAR>i : MeasureTheory.HasFundamentalDomain (↥Γ.op) G ν<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>μ.IsHaarMeasure
<VAR>G : Type u_1<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>PolishSpace G<VAR>Γ : AddSubgroup G<VAR>Countable ↥Γ<VAR>Γ.Normal<VAR>T2Space (G ⧸ Γ)<VAR>SecondCountableTopology (G ⧸ Γ)<VAR>μ : MeasureTheory.Measure (G ⧸ Γ)<VAR>ν : MeasureTheory.Measure G<VAR>ν.IsAddHaarMeasure<VAR>ν.IsAddRightInvariant<VAR>LocallyCompactSpace G<VAR>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ<VAR>i : MeasureTheory.HasAddFundamentalDomain (↥Γ.op) G ν<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>μ.IsAddHaarMeasure
<VAR>G : Type u_1<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>PolishSpace G<VAR>Γ : AddSubgroup G<VAR>Countable ↥Γ<VAR>Γ.Normal<VAR>T2Space (G ⧸ Γ)<VAR>SecondCountableTopology (G ⧸ Γ)<VAR>μ : MeasureTheory.Measure (G ⧸ Γ)<VAR>ν : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite ν<VAR>ν.IsAddHaarMeasure<VAR>ν.IsAddRightInvariant<VAR>𝓕 : Set G<VAR>h𝓕 : MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>μ.IsAddLeftInvariant<VAR>MeasureTheory.SigmaFinite μ<VAR>V : Set (G ⧸ Γ)<VAR>hV : (interior V).Nonempty<VAR>meas_V : MeasurableSet V<VAR>hμK : μ V = ν (QuotientAddGroup.mk ⁻¹' V ∩ 𝓕)<VAR>neTopV : μ V ≠ ⊤<GOAL>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ
<VAR>G : Type u_1<VAR>Group G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>BorelSpace G<VAR>PolishSpace G<VAR>Γ : Subgroup G<VAR>Countable ↥Γ<VAR>Γ.Normal<VAR>T2Space (G ⧸ Γ)<VAR>SecondCountableTopology (G ⧸ Γ)<VAR>μ : MeasureTheory.Measure (G ⧸ Γ)<VAR>ν : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite ν<VAR>ν.IsHaarMeasure<VAR>ν.IsMulRightInvariant<VAR>𝓕 : Set G<VAR>h𝓕 : MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>μ.IsMulLeftInvariant<VAR>MeasureTheory.SigmaFinite μ<VAR>V : Set (G ⧸ Γ)<VAR>hV : (interior V).Nonempty<VAR>meas_V : MeasurableSet V<VAR>hμK : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ 𝓕)<VAR>neTopV : μ V ≠ ⊤<GOAL>MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ
<VAR>G : Type u_1<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>PolishSpace G<VAR>Γ : AddSubgroup G<VAR>Countable ↥Γ<VAR>Γ.Normal<VAR>T2Space (G ⧸ Γ)<VAR>SecondCountableTopology (G ⧸ Γ)<VAR>ν : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite ν<VAR>ν.IsAddHaarMeasure<VAR>ν.IsAddRightInvariant<VAR>K : TopologicalSpace.PositiveCompacts (G ⧸ Γ)<VAR>𝓕 : Set G<VAR>h𝓕 : MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>h𝓕_finite : ν 𝓕 ≠ ⊤<GOAL>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν (ν (QuotientAddGroup.mk ⁻¹' ↑K ∩ 𝓕) • MeasureTheory.Measure.addHaarMeasure K)
<VAR>G : Type u_1<VAR>Group G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>BorelSpace G<VAR>PolishSpace G<VAR>Γ : Subgroup G<VAR>Countable ↥Γ<VAR>Γ.Normal<VAR>T2Space (G ⧸ Γ)<VAR>SecondCountableTopology (G ⧸ Γ)<VAR>ν : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite ν<VAR>ν.IsHaarMeasure<VAR>ν.IsMulRightInvariant<VAR>K : TopologicalSpace.PositiveCompacts (G ⧸ Γ)<VAR>𝓕 : Set G<VAR>h𝓕 : MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>h𝓕_finite : ν 𝓕 ≠ ⊤<GOAL>MeasureTheory.QuotientMeasureEqMeasurePreimage ν (ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕) • MeasureTheory.Measure.haarMeasure K)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Γ : AddSubgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>Countable ↥Γ<VAR>MeasurableSpace (G ⧸ Γ)<VAR>BorelSpace (G ⧸ Γ)<VAR>μ.IsAddRightInvariant<VAR>g : G ⧸ Γ → ℝ≥0∞<VAR>g_ae_measurable : AEMeasurable g (MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕))<GOAL>essSup g (MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕)) = essSup (fun x => g ↑x) μ
<VAR>G : Type u_1<VAR>Group G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>Countable ↥Γ<VAR>MeasurableSpace (G ⧸ Γ)<VAR>BorelSpace (G ⧸ Γ)<VAR>μ.IsMulRightInvariant<VAR>g : G ⧸ Γ → ℝ≥0∞<VAR>g_ae_measurable : AEMeasurable g (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕))<GOAL>essSup g (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)) = essSup (fun x => g ↑x) μ
<VAR>G : Type u_1<VAR>Group G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>Countable ↥Γ<VAR>MeasurableSpace (G ⧸ Γ)<VAR>BorelSpace (G ⧸ Γ)<VAR>μ.IsMulRightInvariant<GOAL>MeasureTheory.Measure.map QuotientGroup.mk μ ≪ MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Γ : AddSubgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>Countable ↥Γ<VAR>MeasurableSpace (G ⧸ Γ)<VAR>BorelSpace (G ⧸ Γ)<VAR>μ.IsAddRightInvariant<GOAL>MeasureTheory.Measure.map QuotientAddGroup.mk μ ≪ MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Γ : AddSubgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>Countable ↥Γ<VAR>MeasurableSpace (G ⧸ Γ)<VAR>BorelSpace (G ⧸ Γ)<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ.IsAddRightInvariant<VAR>f : G → E<VAR>hf₁ : MeasureTheory.Integrable f μ<VAR>hf₂ : MeasureTheory.AEStronglyMeasurable (QuotientAddGroup.automorphize f) (MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕))<GOAL>∫ (x : G), f x ∂μ = ∫ (x : G ⧸ Γ), QuotientAddGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕)