ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>ι : Sort uι<VAR>MeasurableSpace α<VAR>Countable ι<VAR>p : ι → α → Prop<VAR>hp : ∀ (i : ι), Measurable (p i)<GOAL>Measurable fun a => ∀ (i : ι), p i a
<VAR>α : Type u_1<VAR>ι : Sort uι<VAR>MeasurableSpace α<VAR>Countable ι<VAR>p : ι → α → Prop<VAR>hp : ∀ (i : ι), Measurable (p i)<GOAL>Measurable fun a => ∃ i, p i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>g : β → Set α<GOAL>Measurable g ↔ ∀ (a : α), Measurable fun x => a ∈ g x
<VAR>α : Type u_1<VAR>a : α<GOAL>Measurable fun s => a ∈ s
<VAR>α : Type u_1<VAR>a : α<GOAL>Measurable fun s => a ∉ s
<VAR>α : Type u_1<VAR>a : α<GOAL>MeasurableSet {s | a ∈ s}
<VAR>α : Type u_1<VAR>a : α<GOAL>MeasurableSet {s | a ∉ s}
<VAR>α : Type u_1<GOAL>Measurable fun x => xᶜ
<VAR>α : Type u_1<VAR>s : Set α<GOAL>MeasurableSpace.generateFrom {s} = MeasurableSpace.comap (fun x => x ∈ s) ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : Filter α<VAR>self : f.IsMeasurablyGenerated<VAR>s : Set α<GOAL>s ∈ f → ∃ t ∈ f, MeasurableSet t ∧ t ⊆ s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : Filter α<VAR>f.IsMeasurablyGenerated<VAR>p : α → Prop<VAR>h : ∀ᶠ (x : α) in f, p x<GOAL>∃ s ∈ f, MeasurableSet s ∧ ∀ x ∈ s, p x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : Filter α<VAR>f.IsMeasurablyGenerated<VAR>p : Set α → Prop<VAR>h : ∀ᶠ (s : Set α) in f.smallSets, p s<GOAL>∃ s ∈ f, MeasurableSet s ∧ p s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<GOAL>(𝓟 s).IsMeasurablyGenerated ↔ MeasurableSet s
<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<GOAL>∀ {x : MeasurableSpace β} [inst : MeasurableSpace γ] [inst_1 : Countable δ] {l : Filter δ} [inst_2 : l.IsCountablyGenerated] (l' : Filter γ) [inst_3 : l'.IsCountablyGenerated] [hl' : l'.IsMeasurablyGenerated] {f : δ → β → γ}, (∀ (i : δ), Measurable (f i)) → MeasurableSet {x | Filter.Tendsto (fun n => f n x) l l'}
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>IsCountablySpanning {s | MeasurableSet s}
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>a : α<VAR>s : Subtype MeasurableSet<GOAL>a ∈ ↑s ↔ a ∈ s
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>↑∅ = ∅
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>a : α<VAR>s : Subtype MeasurableSet<GOAL>↑(insert a s) = insert a ↑s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>a : α<GOAL>↑{a} = {a}
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Subtype MeasurableSet<GOAL>↑sᶜ = (↑s)ᶜ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s t : Subtype MeasurableSet<GOAL>↑(s ∪ t) = ↑s ∪ ↑t
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s t : { s // MeasurableSet s }<GOAL>s ⊔ t = s ∪ t
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s t : Subtype MeasurableSet<GOAL>↑(s ∩ t) = ↑s ∩ ↑t
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s t : { s // MeasurableSet s }<GOAL>s ⊓ t = s ∩ t
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s t : Subtype MeasurableSet<GOAL>↑(s \ t) = ↑s \ ↑t
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s t : Subtype MeasurableSet<GOAL>↑(s ⇨ t) = ↑s ⇨ ↑t
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>↑⊥ = ⊥
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>↑⊤ = ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : ℕ → Set α<VAR>p : ℕ → Prop<VAR>h : ∀ (n : ℕ), p n → MeasurableSet (s n)<GOAL>MeasurableSet (Filter.blimsup s Filter.atTop p)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : ℕ → Set α<VAR>p : ℕ → Prop<VAR>h : ∀ (n : ℕ), p n → MeasurableSet (s n)<GOAL>MeasurableSet (Filter.bliminf s Filter.atTop p)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : ℕ → Set α<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n)<GOAL>MeasurableSet (Filter.limsup s Filter.atTop)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : ℕ → Set α<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n)<GOAL>MeasurableSet (Filter.liminf s Filter.atTop)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E → F<VAR>R : ℝ<GOAL>∫ (x : E), f (R • x) ∂μ = |(R ^ FiniteDimensional.finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E → F<VAR>R : ℝ<VAR>hR : 0 ≤ R<GOAL>∫ (x : E), f (R • x) ∂μ = (R ^ FiniteDimensional.finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E → F<VAR>R : ℝ<GOAL>∫ (x : E), f (R⁻¹ • x) ∂μ = |R ^ FiniteDimensional.finrank ℝ E| • ∫ (x : E), f x ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E → F<VAR>R : ℝ<VAR>hR : 0 ≤ R<GOAL>∫ (x : E), f (R⁻¹ • x) ∂μ = R ^ FiniteDimensional.finrank ℝ E • ∫ (x : E), f x ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E → F<VAR>R : ℝ<VAR>s : Set E<VAR>hR : R ≠ 0<GOAL>∫ (x : E) in s, f (R • x) ∂μ = |(R ^ FiniteDimensional.finrank ℝ E)⁻¹| • ∫ (x : E) in R • s, f x ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E → F<VAR>R : ℝ<VAR>s : Set E<VAR>hR : 0 < R<GOAL>∫ (x : E) in s, f (R • x) ∂μ = (R ^ FiniteDimensional.finrank ℝ E)⁻¹ • ∫ (x : E) in R • s, f x ∂μ
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>g : ℝ → F<VAR>a : ℝ<GOAL>∫ (x : ℝ), g (a * x) = |a⁻¹| • ∫ (y : ℝ), g y
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>g : ℝ → F<VAR>a : ℝ<GOAL>∫ (x : ℝ), g (a⁻¹ * x) = |a| • ∫ (y : ℝ), g y
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>g : ℝ → F<VAR>a : ℝ<GOAL>∫ (x : ℝ), g (x * a) = |a⁻¹| • ∫ (y : ℝ), g y
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>g : ℝ → F<VAR>a : ℝ<GOAL>∫ (x : ℝ), g (x * a⁻¹) = |a| • ∫ (y : ℝ), g y
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>g : ℝ → F<VAR>a : ℝ<GOAL>∫ (x : ℝ), g (x / a) = |a| • ∫ (y : ℝ), g y
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>f : E → F<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>MeasureTheory.Integrable (fun x => f (R • x)) μ ↔ MeasureTheory.Integrable f μ
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>f : E → F<VAR>hf : MeasureTheory.Integrable f μ<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>MeasureTheory.Integrable (fun x => f (R • x)) μ
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>g : ℝ → F<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>MeasureTheory.Integrable (fun x => g (R * x)) MeasureTheory.volume ↔ MeasureTheory.Integrable g MeasureTheory.volume
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>g : ℝ → F<VAR>hg : MeasureTheory.Integrable g MeasureTheory.volume<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>MeasureTheory.Integrable (fun x => g (R * x)) MeasureTheory.volume
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>g : ℝ → F<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>MeasureTheory.Integrable (fun x => g (x * R)) MeasureTheory.volume ↔ MeasureTheory.Integrable g MeasureTheory.volume
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>g : ℝ → F<VAR>hg : MeasureTheory.Integrable g MeasureTheory.volume<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>MeasureTheory.Integrable (fun x => g (x * R)) MeasureTheory.volume
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>g : ℝ → F<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>MeasureTheory.Integrable (fun x => g (x / R)) MeasureTheory.volume ↔ MeasureTheory.Integrable g MeasureTheory.volume
<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>g : ℝ → F<VAR>hg : MeasureTheory.Integrable g MeasureTheory.volume<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>MeasureTheory.Integrable (fun x => g (x / R)) MeasureTheory.volume
<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>A : Type u_4<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace ℝ E'<VAR>FiniteDimensional ℝ E'<VAR>MeasurableSpace E'<VAR>BorelSpace E'<VAR>NormedAddCommGroup F'<VAR>InnerProductSpace ℝ F'<VAR>FiniteDimensional ℝ F'<VAR>MeasurableSpace F'<VAR>BorelSpace F'<VAR>f : E' ≃ₗᵢ[ℝ] F'<VAR>NormedAddCommGroup A<VAR>g : F' → A<GOAL>MeasureTheory.Integrable (g ∘ ⇑f) MeasureTheory.volume ↔ MeasureTheory.Integrable g MeasureTheory.volume
<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>A : Type u_4<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace ℝ E'<VAR>FiniteDimensional ℝ E'<VAR>MeasurableSpace E'<VAR>BorelSpace E'<VAR>NormedAddCommGroup F'<VAR>InnerProductSpace ℝ F'<VAR>FiniteDimensional ℝ F'<VAR>MeasurableSpace F'<VAR>BorelSpace F'<VAR>f : E' ≃ₗᵢ[ℝ] F'<VAR>NormedAddCommGroup A<VAR>NormedSpace ℝ A<VAR>g : F' → A<GOAL>∫ (x : E'), g (f x) = ∫ (y : F'), g y
<VAR>ι : Type u_1<VAR>F : Type u_3<VAR>Fintype ι<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>n : ℕ<VAR>_i : Fact (FiniteDimensional.finrank ℝ F = n)<VAR>o : Orientation ℝ F (Fin n)<VAR>b : OrthonormalBasis ι ℝ F<GOAL>o.volumeForm.measure (parallelepiped ⇑b) = 1
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>n : ℕ<VAR>_i : Fact (FiniteDimensional.finrank ℝ F = n)<VAR>o : Orientation ℝ F (Fin n)<GOAL>o.volumeForm.measure = MeasureTheory.volume
<VAR>ι : Type u_1<VAR>F : Type u_3<VAR>Fintype ι<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>b : OrthonormalBasis ι ℝ F<GOAL>MeasureTheory.volume (parallelepiped ⇑b) = 1
<VAR>ι : Type u_4<VAR>F : Type u_5<VAR>Fintype ι<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>b : OrthonormalBasis ι ℝ F<GOAL>b.toBasis.addHaar = MeasureTheory.volume
<VAR>ι : Type u_1<VAR>F : Type u_3<VAR>Fintype ι<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>b : OrthonormalBasis ι ℝ F<GOAL>MeasureTheory.MeasurePreserving (⇑b.measurableEquiv) MeasureTheory.volume MeasureTheory.volume
<VAR>ι : Type u_1<VAR>F : Type u_3<VAR>Fintype ι<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>b : OrthonormalBasis ι ℝ F<GOAL>MeasureTheory.MeasurePreserving (⇑b.repr) MeasureTheory.volume MeasureTheory.volume
<VAR>ι : Type u_1<VAR>F : Type u_3<VAR>Fintype ι<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>b : OrthonormalBasis ι ℝ F<GOAL>MeasureTheory.MeasurePreserving (⇑b.repr.symm) MeasureTheory.volume MeasureTheory.volume
<VAR>ι : Type u_4<VAR>Fintype ι<GOAL>MeasureTheory.MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) MeasureTheory.volume MeasureTheory.volume
<VAR>ι : Type u_4<VAR>Fintype ι<GOAL>MeasureTheory.MeasurePreserving (⇑(WithLp.equiv 2 (ι → ℝ))) MeasureTheory.volume MeasureTheory.volume
<VAR>ι : Type u_4<VAR>Fintype ι<GOAL>MeasureTheory.MeasurePreserving (⇑(WithLp.equiv 2 (ι → ℝ)).symm) MeasureTheory.volume MeasureTheory.volume
<VAR>ι : Type u_4<VAR>Fintype ι<VAR>IsEmpty ι<GOAL>MeasureTheory.volume = MeasureTheory.Measure.dirac 0
<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>f : E ≃ₗᵢ[ℝ] F<GOAL>MeasureTheory.MeasurePreserving (⇑f) MeasureTheory.volume MeasureTheory.volume
<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>f : E ≃ₗᵢ[ℝ] F<GOAL>⇑f.toMeasureEquiv = ⇑f
<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>f : E ≃ₗᵢ[ℝ] F<GOAL>f.toMeasureEquiv.symm = f.symm.toMeasureEquiv
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>MeasureTheory.llr μ ν = fun x => Real.log (μ.rnDeriv ν x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>(fun x => rexp (MeasureTheory.llr μ ν x)) =ᵐ[ν] fun x => if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>μ.HaveLebesgueDecomposition ν<VAR>hμν : μ.AbsolutelyContinuous ν<GOAL>(fun x => rexp (MeasureTheory.llr μ ν x)) =ᵐ[μ] fun x => (μ.rnDeriv ν x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : ν.AbsolutelyContinuous μ<GOAL>(fun x => rexp (MeasureTheory.llr μ ν x)) =ᵐ[ν] fun x => (μ.rnDeriv ν x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : μ.AbsolutelyContinuous ν<GOAL>-MeasureTheory.llr μ ν =ᵐ[μ] MeasureTheory.llr ν μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : μ.AbsolutelyContinuous ν<GOAL>(fun x => rexp (-MeasureTheory.llr μ ν x)) =ᵐ[μ] fun x => (ν.rnDeriv μ x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : ν.AbsolutelyContinuous μ<GOAL>(fun x => rexp (-MeasureTheory.llr μ ν x)) =ᵐ[ν] fun x => (ν.rnDeriv μ x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>Measurable (MeasureTheory.llr μ ν)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>MeasureTheory.StronglyMeasurable (MeasureTheory.llr μ ν)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>μ.HaveLebesgueDecomposition ν<VAR>hμν : μ.AbsolutelyContinuous ν<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>hc_ne_top : c ≠ ⊤<GOAL>MeasureTheory.llr (c • μ) ν =ᵐ[μ] fun x => MeasureTheory.llr μ ν x + Real.log c.toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>μ.HaveLebesgueDecomposition ν<VAR>hμν : μ.AbsolutelyContinuous ν<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>hc_ne_top : c ≠ ⊤<GOAL>MeasureTheory.llr μ (c • ν) =ᵐ[μ] fun x => MeasureTheory.llr μ ν x - Real.log c.toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : μ.AbsolutelyContinuous ν<VAR>hf : MeasureTheory.Integrable (fun x => rexp (f x)) μ<VAR>hfν : AEMeasurable f ν<GOAL>MeasureTheory.llr (μ.tilted f) ν =ᵐ[μ] fun x => f x - Real.log (∫ (z : α), rexp (f z) ∂μ) + MeasureTheory.llr μ ν x
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : μ.AbsolutelyContinuous ν<VAR>hf : MeasureTheory.Integrable f μ<VAR>h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ<VAR>hfμ : MeasureTheory.Integrable (fun x => rexp (f x)) μ<VAR>hfν : AEMeasurable f ν<GOAL>MeasureTheory.Integrable (MeasureTheory.llr (μ.tilted f) ν) μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : μ.AbsolutelyContinuous ν<VAR>hf : MeasureTheory.Integrable f μ<VAR>h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ<VAR>hfμ : MeasureTheory.Integrable (fun x => rexp (f x)) μ<VAR>hfν : AEMeasurable f ν<GOAL>∫ (x : α), MeasureTheory.llr (μ.tilted f) ν x ∂μ = ∫ (x : α), MeasureTheory.llr μ ν x ∂μ + ∫ (x : α), f x ∂μ - Real.log (∫ (x : α), rexp (f x) ∂μ)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : μ.AbsolutelyContinuous ν<VAR>hf : MeasureTheory.Integrable (fun x => rexp (f x)) ν<GOAL>MeasureTheory.llr μ (ν.tilted f) =ᵐ[μ] fun x => -f x + Real.log (∫ (z : α), rexp (f z) ∂ν) + MeasureTheory.llr μ ν x
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : μ.AbsolutelyContinuous ν<VAR>hfμ : MeasureTheory.Integrable f μ<VAR>h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ<VAR>hfν : MeasureTheory.Integrable (fun x => rexp (f x)) ν<GOAL>MeasureTheory.Integrable (MeasureTheory.llr μ (ν.tilted f)) μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : μ.AbsolutelyContinuous ν<VAR>hfμ : MeasureTheory.Integrable f μ<VAR>hfν : MeasureTheory.Integrable (fun x => rexp (f x)) ν<VAR>h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ<GOAL>∫ (x : α), MeasureTheory.llr μ (ν.tilted f) x ∂μ = ∫ (x : α), MeasureTheory.llr μ ν x ∂μ - ∫ (x : α), f x ∂μ + Real.log (∫ (x : α), rexp (f x) ∂ν)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>SecondCountableTopology E<VAR>f : α → E<VAR>hf : ∀ (c : E), (fun x => ⟪c, f x⟫_𝕜) =ᵐ[μ] 0<GOAL>f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>t : Set E<VAR>ht : TopologicalSpace.IsSeparable t<VAR>f : α → E<VAR>hf : ∀ (c : NormedSpace.Dual 𝕜 E), (fun x => c (f x)) =ᵐ[μ] 0<VAR>h't : ∀ᵐ (x : α) ∂μ, f x ∈ t<GOAL>f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>SecondCountableTopology E<VAR>f : α → E<VAR>hf : ∀ (c : NormedSpace.Dual 𝕜 E), (fun x => c (f x)) =ᵐ[μ] 0<GOAL>f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_3<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>FirstCountableTopology β<VAR>f : α → β<VAR>c : β<GOAL>(∀ᵐ (x : α) ∂μ, c ≤ f x) ↔ ∀ b < c, μ {x | f x ≤ b} = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ<GOAL>f ≤ᵐ[μ] g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ<GOAL>f ≤ᵐ[μ] g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ<GOAL>f =ᵐ[μ] g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ<GOAL>f =ᵐ[μ] g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<GOAL>0 ≤ᵐ[μ] f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<VAR>hf_le : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ<GOAL>f ≤ᵐ[μ] g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>t : Set α<VAR>hf : MeasureTheory.IntegrableOn f t μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ<GOAL>0 ≤ᵐ[μ.restrict t] f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<GOAL>0 ≤ᵐ[μ] f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.AEFinStronglyMeasurable f μ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<GOAL>0 ≤ᵐ[μ] f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>0 ≤ᵐ[μ.restrict t] f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>f =ᵐ[μ.restrict t] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>f =ᵐ[μ.restrict t] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f g : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn g s μ<VAR>hfg_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>f =ᵐ[μ.restrict t] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>MeasureTheory.SigmaFinite μ<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<GOAL>f =ᵐ[μ] 0