ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : MeasureTheory.Measure Ω<VAR>μs : ι → MeasureTheory.Measure Ω<VAR>E₀ E E₁ : Set Ω<VAR>E₀_subset : E₀ ⊆ E<VAR>subset_E₁ : E ⊆ E₁<VAR>nulldiff : μ (E₁ \ E₀) = 0<VAR>h_E₀ : μ E₀ ≤ Filter.liminf (fun i => (μs i) E₀) L<VAR>h_E₁ : Filter.limsup (fun i => (μs i) E₁) L ≤ μ E₁<GOAL>Filter.Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : MeasureTheory.Measure Ω<VAR>μs : ι → MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) L<VAR>E : Set Ω<VAR>E_nullbdry : μ (frontier E) = 0<GOAL>Filter.Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>HasOuterApproxClosed Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>μs : ι → MeasureTheory.FiniteMeasure Ω<VAR>μs_lim : Filter.Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<GOAL>Filter.limsup (fun i => ↑(μs i) F) L ≤ ↑μ F
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>HasOuterApproxClosed Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<VAR>μs : ι → MeasureTheory.ProbabilityMeasure Ω<VAR>μs_lim : Filter.Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<GOAL>Filter.limsup (fun i => ↑(μs i) F) L ≤ ↑μ F
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>HasOuterApproxClosed Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<VAR>μs : ι → MeasureTheory.ProbabilityMeasure Ω<VAR>μs_lim : Filter.Tendsto μs L (𝓝 μ)<VAR>G : Set Ω<VAR>G_open : IsOpen G<GOAL>↑μ G ≤ Filter.liminf (fun i => ↑(μs i) G) L
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>HasOuterApproxClosed Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<VAR>μs : ι → MeasureTheory.ProbabilityMeasure Ω<VAR>μs_lim : Filter.Tendsto μs L (𝓝 μ)<VAR>E : Set Ω<VAR>E_nullbdry : ↑μ (frontier E) = 0<GOAL>Filter.Tendsto (fun i => ↑(μs i) E) L (𝓝 (↑μ E))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>HasOuterApproxClosed Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<VAR>μs : ι → MeasureTheory.ProbabilityMeasure Ω<VAR>μs_lim : Filter.Tendsto μs L (𝓝 μ)<VAR>E : Set Ω<VAR>E_nullbdry : μ (frontier E) = 0<GOAL>Filter.Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
<VAR>Ω : Type u_1<VAR>PseudoEMetricSpace Ω<VAR>MeasurableSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.SFinite μ<VAR>s : Set Ω<VAR>a b : ℝ<VAR>hab : a < b<GOAL>∃ r ∈ Set.Ioo a b, μ (frontier (Metric.thickening r s)) = 0
<VAR>Ω : Type u_1<VAR>PseudoEMetricSpace Ω<VAR>MeasurableSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.SFinite μ<VAR>s : Set Ω<GOAL>∃ rs, Filter.Tendsto rs Filter.atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) s)) = 0
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>L.NeBot<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>μs : ι → MeasureTheory.Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Filter.Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<GOAL>Filter.limsup (fun i => (μs i) F) L ≤ μ F
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>L.NeBot<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>μs : ι → MeasureTheory.Measure Ω<VAR>∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Filter.Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>G : Set Ω<VAR>G_open : IsOpen G<GOAL>μ G ≤ Filter.liminf (fun i => (μs i) G) L
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>μs : ℕ → MeasureTheory.Measure Ω<VAR>f : Ω → ℝ<VAR>f_cont : Continuous f<VAR>f_nn : 0 ≤ f<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) Filter.atTop<GOAL>∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ Filter.liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) Filter.atTop
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>μs : ℕ → MeasureTheory.Measure Ω<VAR>∀ (i : ℕ), MeasureTheory.IsProbabilityMeasure (μs i)<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) Filter.atTop<GOAL>∫ (x : Ω), f x ∂μ ≤ Filter.liminf (fun i => ∫ (x : Ω), f x ∂μs i) Filter.atTop
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<VAR>μs : ℕ → MeasureTheory.ProbabilityMeasure Ω<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) Filter.atTop<GOAL>Filter.Tendsto (fun i => μs i) Filter.atTop (𝓝 μ)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.trim ⋯ = μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<GOAL>(μ.trim hm).toOuterMeasure = μ.trim
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>hm : m ≤ m0<GOAL>MeasureTheory.Measure.trim 0 hm = 0
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<GOAL>(μ.trim hm) s = μ s
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<GOAL>μ s ≤ (μ.trim hm) s
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>hm : m ≤ m0<GOAL>(μ + ν).trim hm = μ.trim hm + ν.trim hm
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>h : (μ.trim hm) s = 0<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hs : (μ.trim hm) s = 0<GOAL>μ (MeasureTheory.toMeasurable (μ.trim hm) s) = 0
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>hm : m ≤ m0<VAR>μ : MeasureTheory.Measure α<VAR>P : α → Prop<VAR>h : ∀ᵐ (x : α) ∂μ.trim hm, P x<GOAL>∀ᵐ (x : α) ∂μ, P x
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_2<VAR>hm : m ≤ m0<VAR>f₁ f₂ : α → E<VAR>h12 : f₁ =ᵐ[μ.trim hm] f₂<GOAL>f₁ =ᵐ[μ] f₂
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_2<VAR>LE E<VAR>hm : m ≤ m0<VAR>f₁ f₂ : α → E<VAR>h12 : f₁ ≤ᵐ[μ.trim hm] f₂<GOAL>f₁ ≤ᵐ[μ] f₂
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>m₁ m₂ : MeasurableSpace α<VAR>hm₁₂ : m₁ ≤ m₂<VAR>hm₂ : m₂ ≤ m0<GOAL>(μ.trim hm₂).trim hm₁₂ = μ.trim ⋯
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>μ : MeasureTheory.Measure α<VAR>hs : MeasurableSet s<GOAL>(μ.trim hm).restrict s = (μ.restrict s).trim hm
<VAR>α : Type u_1<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>hm₂ : m₂ ≤ m<VAR>MeasureTheory.SigmaFinite (μ.trim ⋯)<GOAL>MeasureTheory.SigmaFinite (μ.trim hm)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.SigmaFinite (μ.trim ⋯) ↔ MeasureTheory.IsFiniteMeasure μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>hμν : μ.AbsolutelyContinuous ν<VAR>hm : m ≤ m0<GOAL>(μ.trim hm).AbsolutelyContinuous (ν.trim hm)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>Measurable fun μ => μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → MeasureTheory.Measure α<VAR>h : ∀ (s : Set α), MeasurableSet s → Measurable fun b => (f b) s<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : α → MeasureTheory.Measure β<GOAL>Measurable μ ↔ ∀ (s : Set β), MeasurableSet s → Measurable fun b => (μ b) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>hf : Measurable f<GOAL>Measurable fun μ => MeasureTheory.Measure.map f μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>Measurable MeasureTheory.Measure.dirac
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Measurable fun μ => ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m : MeasureTheory.Measure (MeasureTheory.Measure α)<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>m.join s = ∫⁻ (μ : MeasureTheory.Measure α), μ s ∂m
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>MeasureTheory.Measure.join 0 = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>Measurable MeasureTheory.Measure.join
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m : MeasureTheory.Measure (MeasureTheory.Measure α)<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : MeasureTheory.Measure α), ∫⁻ (x : α), f x ∂μ ∂m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → MeasureTheory.Measure β<GOAL>MeasureTheory.Measure.bind 0 f = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>m : MeasureTheory.Measure α<GOAL>m.bind 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>m : MeasureTheory.Measure α<GOAL>(m.bind fun x => 0) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>m : MeasureTheory.Measure α<VAR>f : α → MeasureTheory.Measure β<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : Measurable f<GOAL>(m.bind f) s = ∫⁻ (a : α), (f a) s ∂m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>g : α → MeasureTheory.Measure β<VAR>hg : Measurable g<GOAL>Measurable fun m => m.bind g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>m : MeasureTheory.Measure α<VAR>μ : α → MeasureTheory.Measure β<VAR>f : β → ℝ≥0∞<VAR>hμ : Measurable μ<VAR>hf : Measurable f<GOAL>∫⁻ (x : β), f x ∂m.bind μ = ∫⁻ (a : α), ∫⁻ (x : β), f x ∂μ a ∂m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>γ : Type u_3<VAR>MeasurableSpace γ<VAR>m : MeasureTheory.Measure α<VAR>f : α → MeasureTheory.Measure β<VAR>g : β → MeasureTheory.Measure γ<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>(m.bind f).bind g = m.bind fun a => (f a).bind g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → MeasureTheory.Measure β<VAR>hf : Measurable f<VAR>a : α<GOAL>(MeasureTheory.Measure.dirac a).bind f = f a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>m : MeasureTheory.Measure α<GOAL>m.bind MeasureTheory.Measure.dirac = m
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure (MeasureTheory.Measure α)<GOAL>μ.join = μ.bind id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α → β<VAR>hf : Measurable f<VAR>μ : MeasureTheory.Measure (MeasureTheory.Measure α)<GOAL>(MeasureTheory.Measure.map (MeasureTheory.Measure.map f) μ).join = MeasureTheory.Measure.map f μ.join
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure (MeasureTheory.Measure (MeasureTheory.Measure α))<GOAL>(MeasureTheory.Measure.map MeasureTheory.Measure.join μ).join = μ.join.join
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>(MeasureTheory.Measure.map MeasureTheory.Measure.dirac μ).join = μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>(MeasureTheory.Measure.dirac μ).join = μ
<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.condexpIndL1Fin hm hs hμs x) =ᵐ[μ] ↑↑(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>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>MeasureTheory.Memℒp (↑↑(MeasureTheory.condexpIndSMul hm hs hμs x)) 1 μ
<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 y : G<GOAL>MeasureTheory.condexpIndL1Fin hm hs hμs (x + y) = MeasureTheory.condexpIndL1Fin hm hs hμs x + MeasureTheory.condexpIndL1Fin 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>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : ℝ<VAR>x : G<GOAL>MeasureTheory.condexpIndL1Fin hm hs hμs (c • x) = c • MeasureTheory.condexpIndL1Fin hm hs hμs x
<VAR>α : Type u_1<VAR>F : Type u_3<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>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>NormedSpace ℝ F<VAR>SMulCommClass ℝ 𝕜 F<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : 𝕜<VAR>x : F<GOAL>MeasureTheory.condexpIndL1Fin hm hs hμs (c • x) = c • MeasureTheory.condexpIndL1Fin 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>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>‖MeasureTheory.condexpIndL1Fin hm hs hμs x‖ ≤ (μ s).toReal * ‖x‖
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<GOAL>MeasureTheory.condexpIndL1Fin hm ⋯ ⋯ x = MeasureTheory.condexpIndL1Fin hm hs hμs x + MeasureTheory.condexpIndL1Fin hm ht hμ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>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>MeasureTheory.condexpIndL1 hm μ s x = MeasureTheory.condexpIndL1Fin 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>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hμs : μ s = ⊤<VAR>x : G<GOAL>MeasureTheory.condexpIndL1 hm μ s x = 0
<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>x : G<GOAL>MeasureTheory.condexpIndL1 hm μ s x = 0
<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>x y : G<GOAL>MeasureTheory.condexpIndL1 hm μ s (x + y) = MeasureTheory.condexpIndL1 hm μ s x + MeasureTheory.condexpIndL1 hm μ 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>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>c : ℝ<VAR>x : G<GOAL>MeasureTheory.condexpIndL1 hm μ s (c • x) = c • MeasureTheory.condexpIndL1 hm μ s x
<VAR>α : Type u_1<VAR>F : Type u_3<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>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>NormedSpace ℝ F<VAR>SMulCommClass ℝ 𝕜 F<VAR>c : 𝕜<VAR>x : F<GOAL>MeasureTheory.condexpIndL1 hm μ s (c • x) = c • MeasureTheory.condexpIndL1 hm μ 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>x : G<GOAL>‖MeasureTheory.condexpIndL1 hm μ s x‖ ≤ (μ s).toReal * ‖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)<GOAL>Continuous fun x => MeasureTheory.condexpIndL1 hm μ s x
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<GOAL>MeasureTheory.condexpIndL1 hm μ (s ∪ t) x = MeasureTheory.condexpIndL1 hm μ s x + MeasureTheory.condexpIndL1 hm μ 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>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>↑↑((MeasureTheory.condexpInd G hm μ s) x) =ᵐ[μ] ↑↑(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>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>MeasureTheory.AEStronglyMeasurable' m (↑↑((MeasureTheory.condexpInd G hm μ 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>MeasureTheory.SigmaFinite (μ.trim hm)<GOAL>MeasureTheory.condexpInd G hm μ ∅ = 0
<VAR>α : Type u_1<VAR>F : Type u_3<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>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>NormedSpace ℝ F<VAR>SMulCommClass ℝ 𝕜 F<VAR>c : 𝕜<VAR>x : F<GOAL>(MeasureTheory.condexpInd F hm μ s) (c • x) = c • (MeasureTheory.condexpInd F hm μ 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>x : G<GOAL>‖(MeasureTheory.condexpInd G hm μ s) x‖ ≤ (μ s).toReal * ‖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)<GOAL>‖MeasureTheory.condexpInd G hm μ s‖ ≤ (μ s).toReal
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<GOAL>(MeasureTheory.condexpInd G hm μ (s ∪ t)) x = (MeasureTheory.condexpInd G hm μ s) x + (MeasureTheory.condexpInd G hm μ t) x
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<GOAL>MeasureTheory.condexpInd G hm μ (s ∪ t) = MeasureTheory.condexpInd G hm μ s + MeasureTheory.condexpInd G hm μ t
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>m m0 : MeasurableSpace α<VAR>NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<GOAL>MeasureTheory.DominatedFinMeasAdditive μ (MeasureTheory.condexpInd G hm μ) 1
<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>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>x : G'<GOAL>∫ (a : α) in s, ↑↑((MeasureTheory.condexpInd G' hm μ t) x) a ∂μ = (μ (t ∩ s)).toReal • 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>c : G<GOAL>(MeasureTheory.condexpInd G hm μ s) c = MeasureTheory.indicatorConstLp 1 ⋯ hμs c
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>E : Type u_8<VAR>NormedLatticeAddCommGroup E<VAR>NormedSpace ℝ E<VAR>OrderedSMul ℝ E<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E<VAR>hx : 0 ≤ x<GOAL>0 ≤ (MeasureTheory.condexpInd E hm μ s) x
<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 : ↥(MeasureTheory.Lp F' 1 μ)<GOAL>(MeasureTheory.condexpL1CLM F' hm μ) (c • f) = c • (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>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : F'<GOAL>(MeasureTheory.condexpL1CLM F' hm μ) (MeasureTheory.indicatorConstLp 1 hs hμs x) = (MeasureTheory.condexpInd F' hm μ s) 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>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : F'<GOAL>(MeasureTheory.condexpL1CLM F' hm μ) ↑(MeasureTheory.Lp.simpleFunc.indicatorConst 1 hs hμs x) = (MeasureTheory.condexpInd F' hm μ s) 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>s : Set α<VAR>f : ↥(MeasureTheory.Lp F' 1 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>∫ (x : α) in s, ↑↑((MeasureTheory.condexpL1CLM F' 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>s : Set α<VAR>f : ↥(MeasureTheory.Lp F' 1 μ)<VAR>hs : MeasurableSet s<GOAL>∫ (x : α) in s, ↑↑((MeasureTheory.condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ