ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u<VAR>Group G<VAR>n : ℕ<VAR>f : Fin (n + 1) → G<GOAL>(groupCohomology.resolution.actionDiagonalSucc G n).hom.hom f = (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)
<VAR>G : Type u<VAR>Group G<VAR>n : ℕ<VAR>g : G<VAR>f : Fin n → G<GOAL>(groupCohomology.resolution.actionDiagonalSucc G n).inv.hom (g, f) = g • Fin.partialProd f
<VAR>k G : Type u<VAR>CommRing k<VAR>n : ℕ<VAR>Group G<VAR>f : Fin (n + 1) → G<VAR>a : k<GOAL>(groupCohomology.resolution.diagonalSucc k G n).hom.hom (Finsupp.single f a) = Finsupp.single (f 0) 1 ⊗ₜ[k] Finsupp.single (fun i => (f i.castSucc)⁻¹ * f i.succ) a
<VAR>k G : Type u<VAR>CommRing k<VAR>n : ℕ<VAR>Group G<VAR>g : G<VAR>f : Fin n → G<VAR>a b : k<GOAL>(groupCohomology.resolution.diagonalSucc k G n).inv.hom (Finsupp.single g a ⊗ₜ[k] Finsupp.single f b) = Finsupp.single (g • Fin.partialProd f) (a * b)
<VAR>k G : Type u<VAR>CommRing k<VAR>n : ℕ<VAR>Group G<VAR>g : G<VAR>f : (Fin n → G) →₀ k<VAR>r : k<GOAL>(groupCohomology.resolution.diagonalSucc k G n).inv.hom (Finsupp.single g r ⊗ₜ[k] f) = ((Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => Finsupp.single (g • Fin.partialProd f) r) f
<VAR>k G : Type u<VAR>CommRing k<VAR>n : ℕ<VAR>Group G<VAR>g : G →₀ k<VAR>f : Fin n → G<VAR>r : k<GOAL>(groupCohomology.resolution.diagonalSucc k G n).inv.hom (g ⊗ₜ[k] Finsupp.single f r) = ((Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => Finsupp.single (a • Fin.partialProd f) r) g
<VAR>k G : Type u<VAR>CommRing k<VAR>n : ℕ<VAR>Group G<GOAL>Module.Free (MonoidAlgebra k G) (Representation.ofMulAction k G (Fin (n + 1) → G)).asModule
<VAR>k G : Type u<VAR>CommRing k<VAR>n : ℕ<VAR>Group G<VAR>A : Rep k G<VAR>f : Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A<VAR>x : Fin n → G<GOAL>(Rep.diagonalHomEquiv n A) f x = f.hom (Finsupp.single (Fin.partialProd x) 1)
<VAR>k G : Type u<VAR>CommRing k<VAR>n : ℕ<VAR>Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>x : Fin (n + 1) → G<GOAL>((Rep.diagonalHomEquiv n A).symm f).hom (Finsupp.single x 1) = (A.ρ (x 0)) (f fun i => (x i.castSucc)⁻¹ * x i.succ)
<VAR>k G : Type u<VAR>CommRing k<VAR>n : ℕ<VAR>Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>g : Fin (n + 1) → G<VAR>a : Fin (n + 1)<GOAL>((Rep.diagonalHomEquiv n A).symm f).hom (Finsupp.single (Fin.partialProd g ∘ a.succ.succAbove) 1) = f (a.contractNth (fun x x_1 => x * x_1) g)
<VAR>k : Type u<VAR>CommRing k<VAR>G : Type u<VAR>n : ℕ<VAR>c : Fin (n + 1) → G<GOAL>(groupCohomology.resolution.d k G n) (Finsupp.single c 1) = ∑ p : Fin (n + 1), Finsupp.single (c ∘ p.succAbove) ((-1) ^ ↑p)
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>n : ℕ<GOAL>((groupCohomology.resolution k G).d (n + 1) n).hom = groupCohomology.resolution.d k G (n + 1)
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<GOAL>(groupCohomology.resolution.forget₂ToModuleCatHomotopyEquiv k G).hom.f 0 = (CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).map (groupCohomology.resolution.ε k G)
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<GOAL>(groupCohomology.resolution k G).d 1 0 ≫ groupCohomology.resolution.ε k G = 0
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<GOAL>((CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (groupCohomology.resolution.εToSingle₀ k G) ≫ (HomologicalComplex.singleMapHomologicalComplex (CategoryTheory.forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ) 0).hom.app (Rep.trivial k G k) = (groupCohomology.resolution.forget₂ToModuleCatHomotopyEquiv k G).hom
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<GOAL>QuasiIso (((CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (groupCohomology.resolution.εToSingle₀ k G))
<VAR>R : Type u_2<VAR>LinearOrderedRing R<VAR>FloorRing R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>MeasurableSpace R<VAR>OpensMeasurableSpace R<GOAL>Measurable Int.floor
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>MeasurableSpace α<VAR>LinearOrderedRing R<VAR>FloorRing R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>MeasurableSpace R<VAR>OpensMeasurableSpace R<VAR>f : α → R<VAR>hf : Measurable f<GOAL>Measurable fun x => ⌊f x⌋
<VAR>R : Type u_2<VAR>LinearOrderedRing R<VAR>FloorRing R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>MeasurableSpace R<VAR>OpensMeasurableSpace R<GOAL>Measurable Int.ceil
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>MeasurableSpace α<VAR>LinearOrderedRing R<VAR>FloorRing R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>MeasurableSpace R<VAR>OpensMeasurableSpace R<VAR>f : α → R<VAR>hf : Measurable f<GOAL>Measurable fun x => ⌈f x⌉
<VAR>R : Type u_2<VAR>LinearOrderedRing R<VAR>FloorRing R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>MeasurableSpace R<VAR>BorelSpace R<GOAL>Measurable Int.fract
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>MeasurableSpace α<VAR>LinearOrderedRing R<VAR>FloorRing R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>MeasurableSpace R<VAR>BorelSpace R<VAR>f : α → R<VAR>hf : Measurable f<GOAL>Measurable fun x => Int.fract (f x)
<VAR>R : Type u_2<VAR>LinearOrderedRing R<VAR>FloorRing R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>MeasurableSpace R<VAR>BorelSpace R<VAR>s : Set R<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (Int.fract '' s)
<VAR>R : Type u_2<VAR>LinearOrderedSemiring R<VAR>FloorSemiring R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>MeasurableSpace R<VAR>OpensMeasurableSpace R<GOAL>Measurable Nat.floor
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>MeasurableSpace α<VAR>LinearOrderedSemiring R<VAR>FloorSemiring R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>MeasurableSpace R<VAR>OpensMeasurableSpace R<VAR>f : α → R<VAR>hf : Measurable f<GOAL>Measurable fun x => ⌊f x⌋₊
<VAR>R : Type u_2<VAR>LinearOrderedSemiring R<VAR>FloorSemiring R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>MeasurableSpace R<VAR>OpensMeasurableSpace R<GOAL>Measurable Nat.ceil
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>MeasurableSpace α<VAR>LinearOrderedSemiring R<VAR>FloorSemiring R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>MeasurableSpace R<VAR>OpensMeasurableSpace R<VAR>f : α → R<VAR>hf : Measurable f<GOAL>Measurable fun x => ⌈f x⌉₊
<VAR>X : Type u<VAR>MeasurableSpace X<GOAL>↑(MeasCat.of X) = X
<VAR>α : Type u_2<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>IsUnifLocDoublingMeasure μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>K : ℝ<GOAL>IsUnifLocDoublingMeasure.vitaliFamily μ K = let R := IsUnifLocDoublingMeasure.scalingScaleOf μ (max (4 * K + 3) 3); let_fun Rpos := ⋯; let_fun A := ⋯; (Vitali.vitaliFamily μ (IsUnifLocDoublingMeasure.scalingConstantOf μ (max (4 * K + 3) 3)) A).enlarge (R / 4) ⋯
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>IsUnifLocDoublingMeasure μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>K : ℝ<VAR>x y : α<VAR>r : ℝ<VAR>h : dist x y ≤ K * r<VAR>rpos : 0 < r<GOAL>Metric.closedBall y r ∈ (IsUnifLocDoublingMeasure.vitaliFamily μ K).setsAt x
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>IsUnifLocDoublingMeasure μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>K : ℝ<VAR>x : α<VAR>ι : Type u_2<VAR>l : Filter ι<VAR>w : ι → α<VAR>δ : ι → ℝ<VAR>δlim : Filter.Tendsto δ l (𝓝[>] 0)<VAR>xmem : ∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)<GOAL>Filter.Tendsto (fun j => Metric.closedBall (w j) (δ j)) l ((IsUnifLocDoublingMeasure.vitaliFamily μ K).filterAt x)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>IsUnifLocDoublingMeasure μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>S : Set α<VAR>K : ℝ<GOAL>∀ᵐ (x : α) ∂μ.restrict S, ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ), Filter.Tendsto δ l (𝓝[>] 0) → (∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)) → Filter.Tendsto (fun j => μ (S ∩ Metric.closedBall (w j) (δ j)) / μ (Metric.closedBall (w j) (δ j))) l (𝓝 1)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>IsUnifLocDoublingMeasure μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>K : ℝ<GOAL>∀ᵐ (x : α) ∂μ, ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ), Filter.Tendsto δ l (𝓝[>] 0) → (∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)) → Filter.Tendsto (fun j => ⨍ (y : α) in Metric.closedBall (w j) (δ j), ‖f y - f x‖ ∂μ) l (𝓝 0)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>IsUnifLocDoublingMeasure μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : α → E<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>K : ℝ<GOAL>∀ᵐ (x : α) ∂μ, ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ), Filter.Tendsto δ l (𝓝[>] 0) → (∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)) → Filter.Tendsto (fun j => ⨍ (y : α) in Metric.closedBall (w j) (δ j), f y ∂μ) l (𝓝 (f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ConditionallyCompleteLattice β<VAR>f g : α → β<VAR>hfg : f =ᵐ[μ] g<GOAL>essSup f μ = essSup g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ConditionallyCompleteLattice β<VAR>f g : α → β<VAR>hfg : f =ᵐ[μ] g<GOAL>essInf f μ = essInf g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ConditionallyCompleteLattice β<VAR>NeZero μ<VAR>c : β<GOAL>essSup (fun x => c) μ = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ConditionallyCompleteLattice β<VAR>NeZero μ<VAR>c : β<GOAL>essInf (fun x => c) μ = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ConditionallyCompleteLattice β<VAR>c : β<VAR>hμ : μ ≠ 0<GOAL>essSup (fun x => c) μ = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ConditionallyCompleteLattice β<VAR>c : β<VAR>hμ : μ ≠ 0<GOAL>essInf (fun x => c) μ = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLinearOrder β<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<GOAL>essSup f μ = sInf {a | μ {x | a < f x} = 0}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLinearOrder β<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<GOAL>essInf f μ = sSup {a | μ {x | f x < a} = 0}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ConditionallyCompleteLinearOrder β<VAR>x : β<VAR>f : α → β<VAR>hx : essSup f μ < x<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) (MeasureTheory.ae μ) f := by isBoundedDefault<GOAL>∀ᵐ (y : α) ∂μ, f y < x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ConditionallyCompleteLinearOrder β<VAR>x : β<VAR>f : α → β<VAR>hx : x < essInf f μ<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) (MeasureTheory.ae μ) f := by isBoundedDefault<GOAL>∀ᵐ (y : α) ∂μ, x < f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ConditionallyCompleteLinearOrder β<VAR>f : α → β<VAR>TopologicalSpace β<VAR>FirstCountableTopology β<VAR>OrderTopology β<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) (MeasureTheory.ae μ) f := by isBoundedDefault<GOAL>∀ᵐ (y : α) ∂μ, f y ≤ essSup f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ConditionallyCompleteLinearOrder β<VAR>f : α → β<VAR>TopologicalSpace β<VAR>FirstCountableTopology β<VAR>OrderTopology β<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) (MeasureTheory.ae μ) f := by isBoundedDefault<GOAL>∀ᵐ (y : α) ∂μ, essInf f μ ≤ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ConditionallyCompleteLinearOrder β<VAR>f : α → β<VAR>TopologicalSpace β<VAR>FirstCountableTopology β<VAR>OrderTopology β<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) (MeasureTheory.ae μ) f := by isBoundedDefault<GOAL>μ {y | essSup f μ < f y} = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ConditionallyCompleteLinearOrder β<VAR>f : α → β<VAR>TopologicalSpace β<VAR>FirstCountableTopology β<VAR>OrderTopology β<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) (MeasureTheory.ae μ) f := by isBoundedDefault<GOAL>μ {y | f y < essInf f μ} = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice β<VAR>m : MeasurableSpace α<VAR>f : α → β<GOAL>essSup f 0 = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice β<GOAL>∀ {x : MeasurableSpace α} {f : α → β}, essInf f 0 = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteLattice β<VAR>f g : α → β<VAR>hfg : f ≤ᵐ[μ] g<GOAL>essSup f μ ≤ essSup g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteLattice β<VAR>f g : α → β<VAR>hfg : f ≤ᵐ[μ] g<GOAL>essInf f μ ≤ essInf g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteLattice β<VAR>f : α → β<VAR>c : β<VAR>hf : f ≤ᵐ[μ] fun x => c<GOAL>essSup f μ ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteLattice β<VAR>f : α → β<VAR>c : β<VAR>hf : (fun x => c) ≤ᵐ[μ] f<GOAL>c ≤ essInf f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteLattice β<GOAL>essSup (fun x => ⊥) μ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteLattice β<GOAL>essInf (fun x => ⊤) μ = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice β<VAR>m : MeasurableSpace α<VAR>γ : Type u_3<VAR>CompleteLattice γ<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>g : β ≃o γ<GOAL>g (essSup f μ) = essSup (fun x => g (f x)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice β<GOAL>∀ {x : MeasurableSpace α} {γ : Type u_3} [inst : CompleteLattice γ] (f : α → β) (μ : MeasureTheory.Measure α) (g : β ≃o γ), g (essInf f μ) = essInf (fun x => g (f x)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>CompleteLattice β<VAR>f : α → β<VAR>hμν : ν ≪ μ<GOAL>essSup f ν ≤ essSup f μ
<VAR>α : Type u_3<VAR>β : Type u_4<GOAL>∀ {x : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : CompleteLattice β] {f : α → β}, ν ≤ μ → essSup f ν ≤ essSup f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>CompleteLattice β<VAR>f : α → β<VAR>hμν : μ ≪ ν<GOAL>essInf f ν ≤ essInf f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteLattice β<VAR>f : α → β<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<GOAL>essSup f (c • μ) = essSup f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>hf : AEMeasurable f μ<GOAL>essSup (g ∘ f) μ ≤ essSup g (MeasureTheory.Measure.map f μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>hf : MeasurableEmbedding f<GOAL>essSup g (MeasureTheory.Measure.map f μ) = essSup (g ∘ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>SecondCountableTopology β<VAR>OrderClosedTopology β<VAR>OpensMeasurableSpace β<VAR>hg : Measurable g<VAR>hf : AEMeasurable f μ<GOAL>essSup g (MeasureTheory.Measure.map f μ) = essSup (g ∘ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>SecondCountableTopology β<VAR>OrderClosedTopology β<VAR>OpensMeasurableSpace β<VAR>hg : AEMeasurable g (MeasureTheory.Measure.map f μ)<VAR>hf : AEMeasurable f μ<GOAL>essSup g (MeasureTheory.Measure.map f μ) = essSup (g ∘ f) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>g : α → ℝ≥0∞<VAR>hs : MeasurableSet s<GOAL>essSup (s.piecewise f g) μ = max (essSup f (μ.restrict s)) (essSup g (μ.restrict sᶜ))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hs : MeasurableSet s<GOAL>essSup (s.indicator f) μ = essSup f (μ.restrict s)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<GOAL>∀ᵐ (y : α) ∂μ, f y ≤ essSup f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<GOAL>essSup f μ = 0 ↔ f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>essSup (fun x => a * f x) μ = a * essSup f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<GOAL>essSup (f * g) μ ≤ essSup f μ * essSup g μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<GOAL>essSup (f + g) μ ≤ essSup f μ + essSup g μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_3<VAR>Countable ι<VAR>LinearOrder ι<VAR>f : ι → α → ℝ≥0∞<GOAL>essSup (fun x => Filter.liminf (fun n => f n x) Filter.atTop) μ ≤ Filter.liminf (fun n => essSup (fun x => f n x) μ) Filter.atTop
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) (MeasureTheory.ae μ) f<GOAL>↑(essSup f μ) = essSup (fun x => ↑(f x)) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hsf : Function.support f ⊆ s<GOAL>essSup f (μ.restrict s) = essSup f μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ENNReal<VAR>hf : AEMeasurable f μ<VAR>hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1<VAR>hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1<GOAL>∫⁻ (a : α), (f * g) a ∂μ ≤ 1
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ<VAR>f : α → ENNReal<VAR>hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>a : α<GOAL>f a = ENNReal.funMulInvSnorm f p μ a * (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ<VAR>hp0 : 0 < p<VAR>f : α → ENNReal<VAR>a : α<GOAL>ENNReal.funMulInvSnorm f p μ a ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ<VAR>hp0_lt : 0 < p<VAR>f : α → ENNReal<VAR>hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<GOAL>∫⁻ (c : α), ENNReal.funMulInvSnorm f p μ c ^ p ∂μ = 1
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ENNReal<VAR>hf : AEMeasurable f μ<VAR>hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ⊤<VAR>hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0<VAR>hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0<GOAL>∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ<VAR>hp0 : 0 ≤ p<VAR>f : α → ENNReal<VAR>hf : AEMeasurable f μ<VAR>hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0<GOAL>f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ<VAR>hp0 : 0 ≤ p<VAR>f g : α → ENNReal<VAR>hf : AEMeasurable f μ<VAR>hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0<GOAL>∫⁻ (a : α), (f * g) a ∂μ = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p q : ℝ<VAR>hp0_lt : 0 < p<VAR>hq0 : 0 ≤ q<VAR>f g : α → ENNReal<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ⊤<VAR>hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0<GOAL>∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ENNReal<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ENNReal<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>p q : ℝ<VAR>hp : 0 ≤ p<VAR>hq : 0 ≤ q<VAR>hpq : p + q = 1<GOAL>∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Finset ι<VAR>f : ι → α → ENNReal<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<VAR>p : ι → ℝ<VAR>hp : ∑ i ∈ s, p i = 1<VAR>h2p : ∀ i ∈ s, 0 ≤ p i<GOAL>∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Finset ι<VAR>g : α → ENNReal<VAR>f : ι → α → ENNReal<VAR>hg : AEMeasurable g μ<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<VAR>q : ℝ<VAR>p : ι → ℝ<VAR>hpq : q + ∑ i ∈ s, p i = 1<VAR>hq : 0 ≤ q<VAR>hp : ∀ i ∈ s, 0 ≤ p i<GOAL>∫⁻ (a : α), g a ^ q * ∏ i ∈ s, f i a ^ p i ∂μ ≤ (∫⁻ (a : α), g a ∂μ) ^ q * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ<VAR>f g : α → ENNReal<VAR>hf : AEMeasurable f μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤<VAR>hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤<VAR>hp1 : 1 ≤ p<GOAL>∫⁻ (a : α), (f + g) a ^ p ∂μ < ⊤
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>p q r : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq : p < q<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ENNReal<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>(∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ENNReal<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<GOAL>∫⁻ (a : α), f a * g a ^ (p - 1) ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ENNReal<VAR>hf : AEMeasurable f μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤<GOAL>∫⁻ (a : α), (f + g) a ^ p ∂μ ≤ ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) * (∫⁻ (a : α), (f a + g a) ^ p ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ENNReal<VAR>hf : AEMeasurable f μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤<VAR>h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0<VAR>h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ⊤<GOAL>(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ<VAR>f g : α → ENNReal<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hp1 : 1 ≤ p<GOAL>(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)