ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f : ↥(MeasureTheory.Lp F' 1 μ)<GOAL>MeasureTheory.AEStronglyMeasurable' m (↑↑((MeasureTheory.condexpL1CLM F' hm μ) f)) μ
<VAR>α : Type u_1<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f : ↥(MeasureTheory.lpMeas F' ℝ m 1 μ)<GOAL>(MeasureTheory.condexpL1CLM F' hm μ) ↑f = ↑f
<VAR>α : Type u_1<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f : ↥(MeasureTheory.Lp F' 1 μ)<VAR>hfm : MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ<GOAL>(MeasureTheory.condexpL1CLM F' hm μ) f = f
<VAR>α : Type u_1<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f : α → F'<VAR>hf : ¬MeasureTheory.Integrable f μ<GOAL>MeasureTheory.condexpL1 hm μ f = 0
<VAR>α : Type u_1<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f : α → F'<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.condexpL1 hm μ f = (MeasureTheory.condexpL1CLM F' hm μ) (MeasureTheory.Integrable.toL1 f hf)
<VAR>α : Type u_1<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<GOAL>MeasureTheory.condexpL1 hm μ 0 = 0
<VAR>α : Type u_1<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>f : α → F'<VAR>hm : m ≤ m0<GOAL>MeasureTheory.condexpL1 hm 0 f = 0
<VAR>α : Type u_1<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f : α → F'<GOAL>MeasureTheory.AEStronglyMeasurable' m (↑↑(MeasureTheory.condexpL1 hm μ f)) μ
<VAR>α : Type u_1<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → F'<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>h : f =ᵐ[μ] g<GOAL>MeasureTheory.condexpL1 hm μ f = MeasureTheory.condexpL1 hm μ g
<VAR>α : Type u_1<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f : α → F'<GOAL>MeasureTheory.Integrable (↑↑(MeasureTheory.condexpL1 hm μ f)) μ
<VAR>α : Type u_1<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f : α → F'<VAR>s : Set α<VAR>hf : MeasureTheory.Integrable f μ<VAR>hs : MeasurableSet s<GOAL>∫ (x : α) in s, ↑↑(MeasureTheory.condexpL1 hm μ f) x ∂μ = ∫ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>MeasureTheory.condexpL1 hm μ (f + g) = MeasureTheory.condexpL1 hm μ f + MeasureTheory.condexpL1 hm μ g
<VAR>α : Type u_1<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f : α → F'<GOAL>MeasureTheory.condexpL1 hm μ (-f) = -MeasureTheory.condexpL1 hm μ f
<VAR>α : Type u_1<VAR>F' : Type u_4<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>c : 𝕜<VAR>f : α → F'<GOAL>MeasureTheory.condexpL1 hm μ (c • f) = c • MeasureTheory.condexpL1 hm μ f
<VAR>α : Type u_1<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>MeasureTheory.condexpL1 hm μ (f - g) = MeasureTheory.condexpL1 hm μ f - MeasureTheory.condexpL1 hm μ g
<VAR>α : Type u_1<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f : α → F'<VAR>hfm : MeasureTheory.AEStronglyMeasurable' m f μ<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>↑↑(MeasureTheory.condexpL1 hm μ f) =ᵐ[μ] f
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>E : Type u_8<VAR>NormedLatticeAddCommGroup E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>OrderedSMul ℝ E<VAR>f g : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<VAR>hfg : f ≤ᵐ[μ] g<GOAL>↑↑(MeasureTheory.condexpL1 hm μ f) ≤ᵐ[μ] ↑↑(MeasureTheory.condexpL1 hm μ g)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.Lp E 2 μ)<GOAL>MeasureTheory.AEStronglyMeasurable' m (↑↑↑((MeasureTheory.condexpL2 E 𝕜 hm) f)) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(MeasureTheory.Lp E 2 μ)<GOAL>MeasureTheory.IntegrableOn (↑↑↑((MeasureTheory.condexpL2 E 𝕜 hm) f)) s μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : ↥(MeasureTheory.Lp E 2 μ)<GOAL>MeasureTheory.Integrable (↑↑↑((MeasureTheory.condexpL2 E 𝕜 hm) f)) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<GOAL>‖MeasureTheory.condexpL2 E 𝕜 hm‖ ≤ 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.Lp E 2 μ)<GOAL>‖(MeasureTheory.condexpL2 E 𝕜 hm) f‖ ≤ ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.Lp E 2 μ)<GOAL>MeasureTheory.eLpNorm (↑↑↑((MeasureTheory.condexpL2 E 𝕜 hm) f)) 2 μ ≤ MeasureTheory.eLpNorm (↑↑f) 2 μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.Lp E 2 μ)<GOAL>‖↑((MeasureTheory.condexpL2 E 𝕜 hm) f)‖ ≤ ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f g : ↥(MeasureTheory.Lp E 2 μ)<GOAL>⟪↑((MeasureTheory.condexpL2 E 𝕜 hm) f), g⟫_𝕜 = ⟪f, ↑((MeasureTheory.condexpL2 E 𝕜 hm) g)⟫_𝕜
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>↑((MeasureTheory.condexpL2 E 𝕜 hm) (MeasureTheory.indicatorConstLp 2 ⋯ hμs c)) = MeasureTheory.indicatorConstLp 2 ⋯ hμs c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f g : ↥(MeasureTheory.Lp E 2 μ)<VAR>hg : MeasureTheory.AEStronglyMeasurable' m (↑↑g) μ<GOAL>⟪↑((MeasureTheory.condexpL2 E 𝕜 hm) f), g⟫_𝕜 = ⟪f, g⟫_𝕜
<VAR>α : Type u_1<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.Lp 𝕜 2 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>∫ (x : α) in s, ↑↑↑((MeasureTheory.condexpL2 𝕜 𝕜 hm) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(MeasureTheory.Lp ℝ 2 μ)<GOAL>∫⁻ (x : α) in s, ↑‖↑↑↑((MeasureTheory.condexpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(MeasureTheory.Lp ℝ 2 μ)<VAR>hf : ↑↑f =ᵐ[μ.restrict s] 0<GOAL>↑↑↑((MeasureTheory.condexpL2 ℝ ℝ hm) f) =ᵐ[μ.restrict s] 0
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>∫⁻ (a : α) in t, ↑‖↑↑↑((MeasureTheory.condexpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1)) a‖₊ ∂μ ≤ μ (s ∩ t)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.Lp E 2 μ)<VAR>c : E<GOAL>↑↑↑((MeasureTheory.condexpL2 𝕜 𝕜 hm) (MeasureTheory.Memℒp.toLp (fun a => ⟪c, ↑↑f a⟫_𝕜) ⋯)) =ᵐ[μ] fun a => ⟪c, ↑↑↑((MeasureTheory.condexpL2 E 𝕜 hm) f) a⟫_𝕜
<VAR>α : Type u_1<VAR>E' : Type u_3<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>CompleteSpace E'<VAR>NormedSpace ℝ E'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.Lp E' 2 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>∫ (x : α) in s, ↑↑↑((MeasureTheory.condexpL2 E' 𝕜 hm) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>E' : Type u_3<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>CompleteSpace E'<VAR>NormedSpace ℝ E'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>RCLike 𝕜'<VAR>NormedAddCommGroup E''<VAR>InnerProductSpace 𝕜' E''<VAR>CompleteSpace E''<VAR>NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>T : E' →L[ℝ] E''<VAR>f : ↥(MeasureTheory.Lp E' 2 μ)<GOAL>↑↑↑((MeasureTheory.condexpL2 E'' 𝕜' hm) (T.compLp f)) =ᵐ[μ] ↑↑(T.compLp ↑((MeasureTheory.condexpL2 E' 𝕜 hm) f))
<VAR>α : Type u_1<VAR>E' : Type u_3<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>CompleteSpace E'<VAR>NormedSpace ℝ E'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<GOAL>↑↑↑((MeasureTheory.condexpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x)) =ᵐ[μ] fun a => ↑↑↑((MeasureTheory.condexpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1)) a • x
<VAR>α : Type u_1<VAR>E' : Type u_3<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>CompleteSpace E'<VAR>NormedSpace ℝ E'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<GOAL>↑((MeasureTheory.condexpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x)) = (ContinuousLinearMap.toSpanSingleton ℝ x).compLp ↑((MeasureTheory.condexpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1))
<VAR>α : Type u_1<VAR>E' : Type u_3<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>CompleteSpace E'<VAR>NormedSpace ℝ E'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>∫⁻ (a : α) in t, ↑‖↑↑↑((MeasureTheory.condexpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x)) a‖₊ ∂μ ≤ μ (s ∩ t) * ↑‖x‖₊
<VAR>α : Type u_1<VAR>E' : Type u_3<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>CompleteSpace E'<VAR>NormedSpace ℝ E'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<GOAL>∫⁻ (a : α), ↑‖↑↑↑((MeasureTheory.condexpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x)) a‖₊ ∂μ ≤ μ s * ↑‖x‖₊
<VAR>α : Type u_1<VAR>E' : Type u_3<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>CompleteSpace E'<VAR>NormedSpace ℝ E'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<GOAL>MeasureTheory.Integrable (↑↑↑((MeasureTheory.condexpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x))) μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>MeasureTheory.AEStronglyMeasurable' m (↑↑(MeasureTheory.condexpIndSMul hm hs hμs x)) μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x y : G<GOAL>MeasureTheory.condexpIndSMul hm hs hμs (x + y) = MeasureTheory.condexpIndSMul hm hs hμs x + MeasureTheory.condexpIndSMul hm hs hμs y
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : ℝ<VAR>x : G<GOAL>MeasureTheory.condexpIndSMul hm hs hμs (c • x) = c • MeasureTheory.condexpIndSMul hm hs hμs x
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>𝕜 : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>NormedSpace ℝ F<VAR>SMulCommClass ℝ 𝕜 F<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : 𝕜<VAR>x : F<GOAL>MeasureTheory.condexpIndSMul hm hs hμs (c • x) = c • MeasureTheory.condexpIndSMul hm hs hμs x
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>↑↑(MeasureTheory.condexpIndSMul hm hs hμs x) =ᵐ[μ] fun a => ↑↑↑((MeasureTheory.condexpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1)) a • x
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>∫⁻ (a : α) in t, ↑‖↑↑(MeasureTheory.condexpIndSMul hm hs hμs x) a‖₊ ∂μ ≤ μ (s ∩ t) * ↑‖x‖₊
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<GOAL>∫⁻ (a : α), ↑‖↑↑(MeasureTheory.condexpIndSMul hm hs hμs x) a‖₊ ∂μ ≤ μ s * ↑‖x‖₊
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>MeasureTheory.Integrable (↑↑(MeasureTheory.condexpIndSMul hm hs hμs x)) μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>x : G<GOAL>MeasureTheory.condexpIndSMul hm ⋯ ⋯ x = 0
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<GOAL>∫ (x : α) in s, ↑↑↑((MeasureTheory.condexpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 ht hμt 1)) x ∂μ = (μ (t ∩ s)).toReal
<VAR>α : Type u_1<VAR>G' : Type u_6<VAR>NormedAddCommGroup G'<VAR>NormedSpace ℝ G'<VAR>CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>x : G'<GOAL>∫ (a : α) in s, ↑↑(MeasureTheory.condexpIndSMul hm ht hμt x) a ∂μ = (μ (t ∩ s)).toReal • x
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<GOAL>0 ≤ᵐ[μ] ↑↑↑((MeasureTheory.condexpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1))
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>E : Type u_10<VAR>NormedLatticeAddCommGroup E<VAR>NormedSpace ℝ E<VAR>OrderedSMul ℝ E<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E<VAR>hx : 0 ≤ x<GOAL>0 ≤ᵐ[μ] ↑↑(MeasureTheory.condexpIndSMul hm hs hμs x)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>a : α<GOAL>s.indicator 1 a ≤ (MeasureTheory.Measure.dirac a) s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.Measure.dirac a) s = s.indicator 1 a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>a : α<VAR>h : a ∈ s<GOAL>(MeasureTheory.Measure.dirac a) s = 1
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>a : α<VAR>s : Set α<GOAL>(MeasureTheory.Measure.dirac a) s = s.indicator 1 a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>hf : Measurable f<VAR>a : α<GOAL>MeasureTheory.Measure.map f (MeasureTheory.Measure.dirac a) = MeasureTheory.Measure.dirac (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>c : β<GOAL>MeasureTheory.Measure.map (fun x => c) μ = μ Set.univ • MeasureTheory.Measure.dirac c
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>a : α<GOAL>μ.restrict {a} = μ {a} • MeasureTheory.Measure.dirac a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>Countable β<VAR>MeasurableSingletonClass β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : Measurable f<GOAL>MeasureTheory.Measure.map f μ = MeasureTheory.Measure.sum fun b => μ (f ⁻¹' {b}) • MeasureTheory.Measure.dirac b
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>Countable α<VAR>MeasurableSingletonClass α<VAR>μ : MeasureTheory.Measure α<GOAL>(MeasureTheory.Measure.sum fun a => μ {a} • MeasureTheory.Measure.dirac a) = μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>Countable α<VAR>MeasurableSingletonClass α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∑' (x : α), s.indicator (fun x => μ {x}) x = μ s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>s ∈ MeasureTheory.ae (MeasureTheory.Measure.dirac a) ↔ a ∈ s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>a : α<VAR>p : α → Prop<VAR>hp : MeasurableSet {x | p x}<GOAL>(∀ᵐ (x : α) ∂MeasureTheory.Measure.dirac a, p x) ↔ p a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>a : α<GOAL>MeasureTheory.ae (MeasureTheory.Measure.dirac a) = pure a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSingletonClass β<VAR>a : α<VAR>f : α → β<VAR>hf : Measurable f<GOAL>f =ᵐ[MeasureTheory.Measure.dirac a] Function.const α (f a)
<VAR>α : Type u_1<VAR>δ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>a : α<VAR>f : α → δ<GOAL>f =ᵐ[MeasureTheory.Measure.dirac a] Function.const α (f a)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>a : α<VAR>hs : MeasurableSet s<VAR>Decidable (a ∈ s)<GOAL>(MeasureTheory.Measure.dirac a).restrict s = if a ∈ s then MeasureTheory.Measure.dirac a else 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>a : α<VAR>MeasurableSingletonClass α<VAR>Decidable (a ∈ s)<GOAL>(MeasureTheory.Measure.dirac a).restrict s = if a ∈ s then MeasureTheory.Measure.dirac a else 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>x : α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.NoAtoms μ<GOAL>(MeasureTheory.Measure.dirac x).MutuallySingular μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>x y : α<GOAL>MeasureTheory.Measure.dirac x = MeasureTheory.Measure.dirac y ↔ ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>x y : α<GOAL>MeasureTheory.Measure.dirac x ≠ MeasureTheory.Measure.dirac y ↔ ∃ A, MeasurableSet A ∧ x ∈ A ∧ y ∉ A
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.SeparatesPoints α<VAR>x y : α<VAR>x_ne_y : x ≠ y<GOAL>MeasureTheory.Measure.dirac x ≠ MeasureTheory.Measure.dirac y
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.SeparatesPoints α<VAR>x y : α<GOAL>MeasureTheory.Measure.dirac x ≠ MeasureTheory.Measure.dirac y ↔ x ≠ y
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.SeparatesPoints α<VAR>x y : α<GOAL>MeasureTheory.Measure.dirac x = MeasureTheory.Measure.dirac y ↔ x = y
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.SeparatesPoints α<GOAL>Function.Injective fun x => MeasureTheory.Measure.dirac x
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>N : ℕ<VAR>τ : ℝ<VAR>self : Besicovitch.SatelliteConfig α N τ<GOAL>Pairwise fun i j => self.r i ≤ dist (self.c i) (self.c j) ∧ self.r j ≤ τ * self.r i ∨ self.r j ≤ dist (self.c j) (self.c i) ∧ self.r i ≤ τ * self.r j
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>N : ℕ<VAR>τ : ℝ<VAR>self : Besicovitch.SatelliteConfig α N τ<VAR>i : Fin (N + 1)<GOAL>i < Fin.last N → self.r i ≤ dist (self.c i) (self.c (Fin.last N)) ∧ self.r (Fin.last N) ≤ τ * self.r i
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>N : ℕ<VAR>τ : ℝ<VAR>self : Besicovitch.SatelliteConfig α N τ<VAR>i : Fin (N + 1)<GOAL>i < Fin.last N → dist (self.c i) (self.c (Fin.last N)) ≤ self.r i + self.r (Fin.last N)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>N : ℕ<VAR>τ : ℝ<VAR>self : Besicovitch.SatelliteConfig α N τ<VAR>i : Fin N.succ<GOAL>0 < self.r i
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>self : HasBesicovitchCovering α<GOAL>∃ N τ, 1 < τ ∧ IsEmpty (Besicovitch.SatelliteConfig α N τ)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : Besicovitch.SatelliteConfig α N τ<VAR>i : Fin N.succ<GOAL>dist (a.c i) (a.c (Fin.last N)) ≤ a.r i + a.r (Fin.last N)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : Besicovitch.SatelliteConfig α N τ<VAR>i : Fin N.succ<VAR>h : 1 ≤ τ<GOAL>a.r (Fin.last N) ≤ τ * a.r i