awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
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)
inr₁ inr₂ inr₃ 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)
⊢ 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

Premises used: add_le_add_iff_right
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
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), (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)
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
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)
⊢ μ.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

Premises used: Norm.norm, BoundedContinuousFunction.integral_const_sub
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
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
⊢ ‖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

Premises used: MeasureTheory.probReal_univ, smul_eq_mul, one_mul
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
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 ∂μ)
inr₁ inr₂ inr₃ 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 ∂μ)
⊢ 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

Premises used: sub_le_sub_iff_left
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
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
⊢ autoParam (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
    tendsto_of_le_liminf_of_limsup_le._auto_1

Tactic:
bdd_above
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
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
⊢ autoParam (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
    tendsto_of_le_liminf_of_limsup_le._auto_1

Tactic:
exact bdd_above
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
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
⊢ autoParam (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
    tendsto_of_le_liminf_of_limsup_le._auto_3

Tactic:
bdd_below
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
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
⊢ autoParam (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
    tendsto_of_le_liminf_of_limsup_le._auto_3

Tactic:
exact bdd_below
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ circleAverage f c R = HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))

Tactic:
rfl

Premises used: rfl, Real.circleAverage
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
hf : ¬CircleIntegrable f c R
⊢ circleAverage f c R = 0

Tactic:
simp_all [circleAverage, CircleIntegrable, intervalIntegral.integral_undef]

Premises used: CircleIntegrable, intervalIntegral.integral_undef, Real.circleAverage
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ circleAverage f c R = ⨍ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)

Tactic:
simp [circleAverage, interval_average_eq]

Premises used: interval_average_eq, Real.circleAverage
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
inst_2 : CompleteSpace E
rw : HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c 0 θ)) = f c
⊢ circleAverage f c 0 = f c

Tactic:
rw [circleAverage]

Premises used: Real.circleAverage
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
inst_2 : CompleteSpace E
⊢ HSMul.hSMul (β := E) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c 0 θ)) = f c

Tactic:
simp only [circleMap_zero_radius, Function.const_apply,
    intervalIntegral.integral_const, sub_zero,
    ← smul_assoc, smul_eq_mul, inv_mul_cancel₀ (mul_ne_zero two_ne_zero pi_ne_zero),
    one_smul]

Premises used: Function.const_apply, smul_assoc, sub_zero, one_smul, two_ne_zero, circleMap_zero_radius, smul_eq_mul, mul_ne_zero, inv_mul_cancel₀, Real.pi_ne_zero, intervalIntegral.integral_const
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
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)))
⊢ circleAverage (fun (z : ℂ) ↦ f (z + c)) 0 R = circleAverage f c R

Tactic:
unfold circleAverage circleMap

Premises used: circleMap, Real.circleAverage
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
e_a :
  Eq.{u_1 + 1} (α := ℝ → E) (fun (θ : ℝ) ↦ (fun (z : ℂ) ↦ f (z + c)) (0 + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))) fun (θ : ℝ) ↦
    f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))
⊢ 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:
congr
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
e_a : ∀ (θ : ℝ), (fun (z : ℂ) ↦ f (z + c)) (0 + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) = f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))
⊢ Eq.{u_1 + 1} (α := ℝ → E) (fun (θ : ℝ) ↦ (fun (z : ℂ) ↦ f (z + c)) (0 + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))) fun (θ : ℝ) ↦
    f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))

Tactic:
ext θ
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R θ : ℝ
e_a : f ((↑R : ℂ) * cexp ((↑θ : ℂ) * I) + c) = f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))
⊢ (fun (z : ℂ) ↦ f (z + c)) (0 + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) = f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))

Tactic:
simp only [zero_add]

Premises used: zero_add
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R θ : ℝ
e_a : (↑R : ℂ) * cexp ((↑θ : ℂ) * I) + c = c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)
⊢ f ((↑R : ℂ) * cexp ((↑θ : ℂ) * I) + c) = f (c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I))

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R θ : ℝ
⊢ (↑R : ℂ) * cexp ((↑θ : ℂ) * I) + c = c + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
⊢ circleAverage f c R = HSMul.hSMul (β := F) (↑(2 * π) : ℂ)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))

Tactic:
simp [circleAverage, ← coe_smul]

Premises used: Complex.coe_smul, Real.circleAverage
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
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))
⊢ HSMul.hSMul (β := F) (↑(2 * π) : ℂ)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) =
    HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c R θ))

Tactic:
rw [intervalIntegral.integral_smul, mul_inv_rev, smul_smul]

Premises used: smul_smul, intervalIntegral.integral_smul, mul_inv_rev
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
match_scalars : (2 * (↑π : ℂ))⁻¹ * 1 = I⁻¹ * (2 * (↑π : ℂ))⁻¹ * I * 1
⊢ 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:
match_scalars
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
⊢ (2 * (↑π : ℂ))⁻¹ * 1 = I⁻¹ * (2 * (↑π : ℂ))⁻¹ * I * 1

Tactic:
field
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
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 θ)))
⊢ 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)

Tactic:
unfold circleIntegral

Premises used: circleIntegral
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
e_a :
  ∀ (θ : ℝ),
    I • f (circleMap c R θ) =
      HSMul.hSMul (β := F) (deriv (circleMap c R) θ) ((fun (z : ℂ) ↦ (z - c)⁻¹ • f z) (circleMap c R θ))
⊢ 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:
congr with θ
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
θ : ℝ
e_a : I • f (circleMap c R θ) = (circleMap 0 R θ * I * (circleMap 0 R θ)⁻¹) • f (circleMap c R θ)
⊢ I • f (circleMap c R θ) =
    HSMul.hSMul (β := F) (deriv (circleMap c R) θ) ((fun (z : ℂ) ↦ (z - c)⁻¹ • f z) (circleMap c R θ))

Tactic:
simp [deriv_circleMap, circleMap_sub_center, smul_smul]

Premises used: circleMap_sub_center, smul_smul, deriv_circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
θ : ℝ
⊢ I • f (circleMap c R θ) = (circleMap 0 R θ * I * (circleMap 0 R θ)⁻¹) • f (circleMap c R θ)

Tactic:
field_simp [circleMap_ne_center h]

Premises used: circleMap_ne_center
-- Module: Mathlib.MeasureTheory.Integral.CircleAverage
Goal:
c : ℂ
R : ℝ
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
calc : circleAverage f c R = HSMul.hSMul (β := F) (↑(2 * π) : ℂ)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
calc₁ :
  HSMul.hSMul (β := F) (↑(2 * π) : ℂ)⁻¹ (∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)) =
    HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c R θ))
calc₂ :
  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)
⊢ circleAverage f c R = HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z)

Tactic:
calc circleAverage f c R
  _ = (↑(2 * π) : ℂ)⁻¹ • ∫ θ in 0..2 * π, f (circleMap c R θ) := by
    simp [circleAverage, ← coe_smul]
  _ = (2 * π * I)⁻¹ • ∫ θ in 0..2 * π, I • f (circleMap c R θ) := by
    rw [intervalIntegral.integral_smul, mul_inv_rev, smul_smul]
    match_scalars
    field
  _ = (2 * π * I)⁻¹ • (∮ z in C(c, R), (z - c)⁻¹ • f z) := by
    unfold circleIntegral
    congr with θ
    simp [deriv_circleMap, circleMap_sub_center, smul_smul]
    field_simp [circleMap_ne_center h]

Premises used: Real.pi, HMul.hMul, HSub.hSub, Complex.ofReal, Inv.inv, circleIntegral, HSMul.hSMul, OfNat.ofNat, Complex.I, Real.circleAverage