awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
⊢ LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
have key : LE.le (α := ℝ) (∫ (x : X), (f + const X ‖f‖ : (a : X) → ℝ) x ∂μ)
  (liminf (fun (i : ι) ↦ ∫ (x : X), (f + const X ‖f‖ : (a : X) → ℝ) x ∂μs i) L)
Tactic: have key := h _ (f.add_norm_nonneg)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key :
  LE.le (α := ℝ) (∫ (x : X), (f + const X ‖f‖ : (a : X) → ℝ) x ∂μ)
    (liminf (fun (i : ι) ↦ ∫ (x : X), (f + const X ‖f‖ : (a : X) → ℝ) x ∂μs i) L)
⊢ LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
have key₁ : ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + μ.real Set.univ • ‖f‖ ≤
  liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + (μs i).real Set.univ • ‖f‖) L
Tactic: simp_rw [f.integral_add_const ‖f‖] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key :
  ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + μ.real Set.univ • ‖f‖ ≤
    liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + (μs i).real Set.univ • ‖f‖) L
⊢ LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
have key₁ : ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖ ≤ liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + ‖f‖) L
Tactic: simp only [probReal_univ, smul_eq_mul, one_mul] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key : ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖ ≤ liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + ‖f‖) L
⊢ LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
have this : liminf (fun (i : ι) ↦ (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i + ‖f‖) L =
  liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖
Tactic: have := liminf_add_const L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above.isCobounded_ge bdd_below
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key : ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖ ≤ liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + ‖f‖) L
this :
  liminf (fun (i : ι) ↦ (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i + ‖f‖) L =
    liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖
⊢ LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
have inr : ∀ (key : ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖ ≤ liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖)
  (this :
    liminf (fun (i : ι) ↦ (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i + ‖f‖) L =
      liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖),
  LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
Tactic: rwa [this, add_le_add_iff_right] at key
Cleared hypotheses: key, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key : ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖ ≤ liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + ‖f‖) L
this :
  liminf (fun (i : ι) ↦ (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i + ‖f‖) L =
    liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖
inr :
  ∀
    (key :
      ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖ ≤ liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖)
    (this :
      liminf (fun (i : ι) ↦ (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i + ‖f‖) L =
        liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖),
    LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
⊢ LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
have inr₁ : ∀
  (key :
    LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L))
  (this :
    liminf (fun (i : ι) ↦ (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i + ‖f‖) L =
      liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖),
  LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
Tactic: rwa [this, add_le_add_iff_right] at key
Cleared hypotheses: key, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
⊢ LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
have key : LE.le (α := ℝ) (∫ (x : X), (const X ‖f‖ - f : (a : X) → ℝ) x ∂μ)
  (liminf (fun (i : ι) ↦ ∫ (x : X), (const X ‖f‖ - f : (a : X) → ℝ) x ∂μs i) L)
Tactic: have key := h _ (f.norm_sub_nonneg)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key :
  LE.le (α := ℝ) (∫ (x : X), (const X ‖f‖ - f : (a : X) → ℝ) x ∂μ)
    (liminf (fun (i : ι) ↦ ∫ (x : X), (const X ‖f‖ - f : (a : X) → ℝ) x ∂μs i) L)
⊢ LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
have key₁ : μ.real Set.univ • ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ ≤
  liminf (fun (i : ι) ↦ (μs i).real Set.univ • ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L
Tactic: simp_rw [f.integral_const_sub ‖f‖] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key :
  μ.real Set.univ • ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ ≤
    liminf (fun (i : ι) ↦ (μs i).real Set.univ • ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L
⊢ LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
have key₁ : ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ ≤ liminf (fun (i : ι) ↦ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L
Tactic: simp only [probReal_univ, smul_eq_mul, one_mul] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key : ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ ≤ liminf (fun (i : ι) ↦ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L
⊢ LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
have this : liminf (fun (i : ι) ↦ ‖f‖ - (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i) L =
  ‖f‖ - limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L
Tactic: have := liminf_const_sub L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above bdd_below.isCobounded_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key : ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ ≤ liminf (fun (i : ι) ↦ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L
this :
  liminf (fun (i : ι) ↦ ‖f‖ - (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i) L =
    ‖f‖ - limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L
⊢ LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
have inr : ∀ (key : ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ ≤ ‖f‖ - limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
  (this :
    liminf (fun (i : ι) ↦ ‖f‖ - (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i) L =
      ‖f‖ - limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L),
  LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
Tactic: rwa [this, sub_le_sub_iff_left] at key
Cleared hypotheses: key, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key : ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ ≤ liminf (fun (i : ι) ↦ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L
this :
  liminf (fun (i : ι) ↦ ‖f‖ - (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i) L =
    ‖f‖ - limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L
inr :
  ∀
    (key :
      ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ ≤ ‖f‖ - limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
    (this :
      liminf (fun (i : ι) ↦ ‖f‖ - (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i) L =
        ‖f‖ - limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L),
    LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
⊢ LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
have inr₁ : ∀
  (key :
    LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
  (this :
    liminf (fun (i : ι) ↦ ‖f‖ - (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i) L =
      ‖f‖ - limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L),
  LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
Tactic: rwa [this, sub_le_sub_iff_left] at key
Cleared hypotheses: key, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
inst_2 : CompleteSpace E
⊢ circleAverage f c 0 = f c
have rw : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c 0 θ)) = f c
Tactic: rw [circleAverage]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ circleAverage (fun (z : ℂ) ↦ f (z + c)) 0 R = circleAverage f c R
have unfold : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, (fun (z : ℂ) ↦ f (z + c)) (0 + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))) =
  HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)))
Tactic: unfold circleAverage circleMap
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹
      (∫ (θ : ℝ) in 0..2 * π, (fun (z : ℂ) ↦ f (z + c)) (0 + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))) =
    HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)))
have e_a : Eq.{u_1 + 1} (α := ℝ → E) (fun (θ : ℝ) ↦ (fun (z : ℂ) ↦ f (z + c)) (0 + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))) fun (θ : ℝ) ↦
  f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ Eq.{u_1 + 1} (α := ℝ → E) (fun (θ : ℝ) ↦ (fun (z : ℂ) ↦ f (z + c)) (0 + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))) fun (θ : ℝ) ↦
    f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))
have e_a : ∀ (θ : ℝ), (fun (z : ℂ) ↦ f (z + c)) (0 + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) = f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))
Tactic: ext θ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R θ : ℝ
⊢ (fun (z : ℂ) ↦ f (z + c)) (0 + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) = f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))
have e_a : f ((↑R : ℂ) * cexp ((↑θ : ℂ) * I) + c) = f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))
Tactic: simp only [zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R θ : ℝ
⊢ f ((↑R : ℂ) * cexp ((↑θ : ℂ) * I) + c) = f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))
have e_a : (↑R : ℂ) * cexp ((↑θ : ℂ) * I) + c = c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
⊢ HSMul.hSMul (β := F) (↑(2 * π) : ℂ)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) =
    HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c R θ))
have rw : HSMul.hSMul (β := F) (↑(2 * π) : ℂ)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) =
  HSMul.hSMul (β := F) (I⁻¹ * (2 * (↑π : ℂ))⁻¹ * I) (∫ (x : ℝ) in 0..2 * π, f (circleMap c R x))
Tactic: rw [intervalIntegral.integral_smul, mul_inv_rev, smul_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
⊢ HSMul.hSMul (β := F) (↑(2 * π) : ℂ)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) =
    HSMul.hSMul (β := F) (I⁻¹ * (2 * (↑π : ℂ))⁻¹ * I) (∫ (x : ℝ) in 0..2 * π, f (circleMap c R x))
have match_scalars : (2 * (↑π : ℂ))⁻¹ * 1 = I⁻¹ * (2 * (↑π : ℂ))⁻¹ * I * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
⊢ HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c R θ)) =
    HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z)
have unfold : HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c R θ)) =
  HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹
    (∫ (θ : ℝ) in 0..2 * π,
      HSMul.hSMul (β := F) (deriv (circleMap c R) θ) ((fun (z : ℂ) ↦ (z - c)⁻¹ • f z) (circleMap c R θ)))
Tactic: unfold circleIntegral
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
⊢ HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c R θ)) =
    HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹
      (∫ (θ : ℝ) in 0..2 * π,
        HSMul.hSMul (β := F) (deriv (circleMap c R) θ) ((fun (z : ℂ) ↦ (z - c)⁻¹ • f z) (circleMap c R θ)))
have e_a : ∀ (θ : ℝ),
  I • f (circleMap c R θ) =
    HSMul.hSMul (β := F) (deriv (circleMap c R) θ) ((fun (z : ℂ) ↦ (z - c)⁻¹ • f z) (circleMap c R θ))
Tactic: congr with θ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleAverage (goal)
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
θ : ℝ
⊢ I • f (circleMap c R θ) =
    HSMul.hSMul (β := F) (deriv (circleMap c R) θ) ((fun (z : ℂ) ↦ (z - c)⁻¹ • f z) (circleMap c R θ))
have e_a : I • f (circleMap c R θ) = (circleMap 0 R θ * I * (circleMap 0 R θ)⁻¹) • f (circleMap c R θ)
Tactic: simp [deriv_circleMap, circleMap_sub_center, smul_smul]