awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
⊢ eLpNorm (Set.indicator {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} (f i)) p μ =
    eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ
have this : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C sorry ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
Tactic: have : {x | (⟨C, hC₁.le⟩ : ℝ≥0) ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖} := by
    ext x
    simp_rw [← norm_toNNReal]
    exact Real.le_toNNReal_iff_coe_le (norm_nonneg _)
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
⊢ eLpNorm (Set.indicator {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} (f i)) p μ =
    eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ
have pos : eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖Set.indicator {x : α | C ≤ ‖f i x‖} (f i) x‖) p μ =
  eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j) x‖) p μ
Tactic: rw [this, ← eLpNorm_norm, ← eLpNorm_norm (Set.indicator _ _)]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖Set.indicator {x : α | C ≤ ‖f i x‖} (f i) x‖) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j) x‖) p μ
have pos : eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f i x‖} (fun (a : α) ↦ ‖f i a‖) x) p μ =
  eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f j x‖} (fun (a : α) ↦ ‖f j a‖) x) p μ
Tactic: simp_rw [norm_indicator_eq_indicator_norm, coe_nnnorm]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
F : E → ℝ := fun (x : E) ↦ if Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖x‖₊ then ‖x‖ else 0
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f i x‖} (fun (a : α) ↦ ‖f i a‖) x) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f j x‖} (fun (a : α) ↦ ‖f j a‖) x) p μ
have F_meas : Measurable F
Tactic: have F_meas : Measurable F := by
    apply measurable_norm.indicator (measurableSet_le measurable_const measurable_nnnorm)
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
F : E → ℝ := fun (x : E) ↦ if Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖x‖₊ then ‖x‖ else 0
F_meas : Measurable F
k : ι
⊢ (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f k x‖} (fun (a : α) ↦ ‖f k a‖) x) = F ∘ f k
have h : ∀ (x : α), Set.indicator {x : α | C ≤ ‖f k x‖} (fun (a : α) ↦ ‖f k a‖) x = (F ∘ f k) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
F : E → ℝ := fun (x : E) ↦ if Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖x‖₊ then ‖x‖ else 0
F_meas : Measurable F
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f i x‖} (fun (a : α) ↦ ‖f i a‖) x) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f j x‖} (fun (a : α) ↦ ‖f j a‖) x) p μ
have this₁ : ∀ (k : ι), (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f k x‖} (fun (a : α) ↦ ‖f k a‖) x) = F ∘ f k
Tactic: have : ∀ k, (fun x ↦ Set.indicator {x | C ≤ ‖f k x‖} (fun a ↦ ‖f k a‖) x) = F ∘ f k := by
    intro k
    ext x
    simp only [Set.indicator, Set.mem_setOf_eq]; norm_cast
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this_1 : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
F : E → ℝ := fun (x : E) ↦ if Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖x‖₊ then ‖x‖ else 0
F_meas : Measurable F
this : ∀ (k : ι), (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f k x‖} (fun (a : α) ↦ ‖f k a‖) x) = F ∘ f k
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f i x‖} (fun (a : α) ↦ ‖f i a‖) x) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f j x‖} (fun (a : α) ↦ ‖f j a‖) x) p μ
have pos : eLpNorm (F ∘ f i) p μ =
  eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f j x‖} (fun (a : α) ↦ ‖f j a‖) x) p μ
Tactic: rw [this, this, ← eLpNorm_map_measure F_meas.aestronglyMeasurable (hf i).aemeasurable_fst,
    (hf i).map_eq, eLpNorm_map_measure F_meas.aestronglyMeasurable (hf j).aemeasurable_fst]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this_1 : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
F : E → ℝ := fun (x : E) ↦ if Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖x‖₊ then ‖x‖ else 0
F_meas : Measurable F
this : ∀ (k : ι), (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f k x‖} (fun (a : α) ↦ ‖f k a‖) x) = F ∘ f k
pos :
  eLpNorm (F ∘ f i) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f j x‖} (fun (a : α) ↦ ‖f j a‖) x) p μ
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f i x‖} (fun (a : α) ↦ ‖f i a‖) x) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f j x‖} (fun (a : α) ↦ ‖f j a‖) x) p μ
have pos₁ : eLpNorm (F ∘ f i) p μ = eLpNorm (F ∘ f j) p μ
Tactic: rw [this, this, ← eLpNorm_map_measure F_meas.aestronglyMeasurable (hf i).aemeasurable_fst,
    (hf i).map_eq, eLpNorm_map_measure F_meas.aestronglyMeasurable (hf j).aemeasurable_fst]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this_1 : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
F : E → ℝ := fun (x : E) ↦ if Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖x‖₊ then ‖x‖ else 0
F_meas : Measurable F
this : ∀ (k : ι), (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f k x‖} (fun (a : α) ↦ ‖f k a‖) x) = F ∘ f k
pos :
  eLpNorm (F ∘ f i) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f j x‖} (fun (a : α) ↦ ‖f j a‖) x) p μ
pos₁ : eLpNorm (F ∘ f i) p μ = eLpNorm (F ∘ f j) p μ
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f i x‖} (fun (a : α) ↦ ‖f i a‖) x) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f j x‖} (fun (a : α) ↦ ‖f j a‖) x) p μ
have pos₂ : @eLpNorm _ _ _ inst_1 F p (Measure.map (f i) μ) = eLpNorm (F ∘ f j) p μ
Tactic: rw [this, this, ← eLpNorm_map_measure F_meas.aestronglyMeasurable (hf i).aemeasurable_fst,
    (hf i).map_eq, eLpNorm_map_measure F_meas.aestronglyMeasurable (hf j).aemeasurable_fst]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this_1 : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
F : E → ℝ := fun (x : E) ↦ if Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖x‖₊ then ‖x‖ else 0
F_meas : Measurable F
this : ∀ (k : ι), (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f k x‖} (fun (a : α) ↦ ‖f k a‖) x) = F ∘ f k
pos :
  eLpNorm (F ∘ f i) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f j x‖} (fun (a : α) ↦ ‖f j a‖) x) p μ
pos₁ : eLpNorm (F ∘ f i) p μ = eLpNorm (F ∘ f j) p μ
pos₂ : @eLpNorm _ _ _ inst_1 F p (Measure.map (f i) μ) = eLpNorm (F ∘ f j) p μ
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f i x‖} (fun (a : α) ↦ ‖f i a‖) x) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f j x‖} (fun (a : α) ↦ ‖f j a‖) x) p μ
have pos₃ : @eLpNorm _ _ _ inst_1 F p (Measure.map (f j) μ) = eLpNorm (F ∘ f j) p μ
Tactic: rw [this, this, ← eLpNorm_map_measure F_meas.aestronglyMeasurable (hf i).aemeasurable_fst,
    (hf i).map_eq, eLpNorm_map_measure F_meas.aestronglyMeasurable (hf j).aemeasurable_fst]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this_1 : Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
F : E → ℝ := fun (x : E) ↦ if Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖x‖₊ then ‖x‖ else 0
F_meas : Measurable F
this : ∀ (k : ι), (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f k x‖} (fun (a : α) ↦ ‖f k a‖) x) = F ∘ f k
pos :
  eLpNorm (F ∘ f i) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f j x‖} (fun (a : α) ↦ ‖f j a‖) x) p μ
pos₁ : eLpNorm (F ∘ f i) p μ = eLpNorm (F ∘ f j) p μ
pos₂ : @eLpNorm _ _ _ inst_1 F p (Measure.map (f i) μ) = eLpNorm (F ∘ f j) p μ
pos₃ : @eLpNorm _ _ _ inst_1 F p (Measure.map (f j) μ) = eLpNorm (F ∘ f j) p μ
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f i x‖} (fun (a : α) ↦ ‖f i a‖) x) p μ =
    eLpNorm (ε := ℝ) (fun (x : α) ↦ Set.indicator {x : α | C ≤ ‖f j x‖} (fun (a : α) ↦ ‖f j a‖) x) p μ
have pos₄ : eLpNorm (F ∘ f j) p μ = eLpNorm (F ∘ f j) p μ
Tactic: rw [this, this, ← eLpNorm_map_measure F_meas.aestronglyMeasurable (hf i).aemeasurable_fst,
    (hf i).map_eq, eLpNorm_map_measure F_meas.aestronglyMeasurable (hf j).aemeasurable_fst]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
⊢ UniformIntegrable f p μ
have hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
Tactic: have hfmeas : ∀ i, AEStronglyMeasurable (f i) μ := fun i =>
    (hf i).aestronglyMeasurable_iff.2 hℒp.1
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
g : ι → α → E := fun (i : ι) ↦ Exists.choose (p := fun (g : α → E) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
⊢ UniformIntegrable f p μ
have hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
Tactic: have hgmeas : ∀ i, StronglyMeasurable (g i) := fun i => (Exists.choose_spec <| hfmeas i).1
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
g : ι → α → E := fun (i : ι) ↦ Exists.choose (p := fun (g : α → E) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
⊢ UniformIntegrable f p μ
have hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i
Tactic: have hgeq : ∀ i, g i =ᵐ[μ] f i := fun i => (Exists.choose_spec <| hfmeas i).2.symm
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
g : ι → α → E := fun (i : ι) ↦ Exists.choose (p := fun (g : α → E) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i
⊢ UniformIntegrable f p μ
have hgℒp : MemLp (g j) p μ
Tactic: have hgℒp : MemLp (g j) p μ := hℒp.ae_eq (hgeq j).symm
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
inst_3 : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (γ := α × β) (fun (ω : γ) ↦ (X ω, Y ω)) (fun (ω : δ) ↦ (X' ω, Y' ω)) μ μ'
⊢ X' ⟂ᵢ[μ'] Y'
have rw : Eq (α := Measure (α × β)) (Measure.prod (Measure.map X μ) (Measure.map Y μ))
  (Measure.prod (Measure.map X' μ') (Measure.map Y' μ'))
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map, ← h_ident.map_eq, h_indep.map_prod_eq_prod_map_map]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
inst_3 : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (γ := α × β) (fun (ω : γ) ↦ (X ω, Y ω)) (fun (ω : δ) ↦ (X' ω, Y' ω)) μ μ'
rw :
  Eq (α := Measure (α × β)) (Measure.prod (Measure.map X μ) (Measure.map Y μ))
    (Measure.prod (Measure.map X' μ') (Measure.map Y' μ'))
⊢ X' ⟂ᵢ[μ'] Y'
have hf : AEMeasurable X μ
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map, ← h_ident.map_eq, h_indep.map_prod_eq_prod_map_map]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
inst_3 : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (γ := α × β) (fun (ω : γ) ↦ (X ω, Y ω)) (fun (ω : δ) ↦ (X' ω, Y' ω)) μ μ'
rw :
  Eq (α := Measure (α × β)) (Measure.prod (Measure.map X μ) (Measure.map Y μ))
    (Measure.prod (Measure.map X' μ') (Measure.map Y' μ'))
hf : AEMeasurable X μ
⊢ X' ⟂ᵢ[μ'] Y'
have hg : AEMeasurable Y μ
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map, ← h_ident.map_eq, h_indep.map_prod_eq_prod_map_map]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
inst_3 : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (γ := α × β) (fun (ω : γ) ↦ (X ω, Y ω)) (fun (ω : δ) ↦ (X' ω, Y' ω)) μ μ'
rw :
  Eq (α := Measure (α × β)) (Measure.prod (Measure.map X μ) (Measure.map Y μ))
    (Measure.prod (Measure.map X' μ') (Measure.map Y' μ'))
hf : AEMeasurable X μ
hg : AEMeasurable Y μ
⊢ X' ⟂ᵢ[μ'] Y'
have hf₁ : AEMeasurable X' μ'
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map, ← h_ident.map_eq, h_indep.map_prod_eq_prod_map_map]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
inst_3 : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (γ := α × β) (fun (ω : γ) ↦ (X ω, Y ω)) (fun (ω : δ) ↦ (X' ω, Y' ω)) μ μ'
rw :
  Eq (α := Measure (α × β)) (Measure.prod (Measure.map X μ) (Measure.map Y μ))
    (Measure.prod (Measure.map X' μ') (Measure.map Y' μ'))
hf : AEMeasurable X μ
hg : AEMeasurable Y μ
hf₁ : AEMeasurable X' μ'
⊢ X' ⟂ᵢ[μ'] Y'
have hg₁ : AEMeasurable Y' μ'
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map, ← h_ident.map_eq, h_indep.map_prod_eq_prod_map_map]
-- Lean 4 proof step from Mathlib.Probability.IdentDistribIndep (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
⊢ IsFiniteMeasure (m0 := mE) (Measure.map Z ν)
have rw : IsFiniteMeasure (m0 := mE) (Measure.map X μ)
Tactic: rw [← hXZ.map_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistribIndep (hypothesis)
Goal:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
⊢ IsFiniteMeasure ν
have this : IsFiniteMeasure (m0 := mE) (Measure.map Z ν)
Tactic: have : IsFiniteMeasure (ν.map Z) := by rw [← hXZ.map_eq]; infer_instance
-- Lean 4 proof step from Mathlib.Probability.IdentDistribIndep (hypothesis)
Goal:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
⊢ Eq (α := Measure (E × F)) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) μ) (Measure.map (fun (ω' : Ω') ↦ (Z ω', W ω')) ν)
have this : IsFiniteMeasure ν
Tactic: have : IsFiniteMeasure ν := by
      have : IsFiniteMeasure (ν.map Z) := by rw [← hXZ.map_eq]; infer_instance
      exact Measure.isFiniteMeasure_of_map hXZ.aemeasurable_snd
-- Lean 4 proof step from Mathlib.Probability.IdentDistribIndep (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
this : IsFiniteMeasure ν
⊢ Eq (α := Measure (E × F)) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) μ) (Measure.map (fun (ω' : Ω') ↦ (Z ω', W ω')) ν)
have rw : Eq (α := Measure (E × F)) (Measure.prod (Measure.map X μ) (Measure.map Y μ))
  (Measure.map (fun (ω' : Ω') ↦ (Z ω', W ω')) ν)
Tactic: rw [hXY.map_prod_eq_prod_map_map hXZ.aemeasurable_fst hYW.aemeasurable_fst,
      hZW.map_prod_eq_prod_map_map hXZ.aemeasurable_snd hYW.aemeasurable_snd,
      hXZ.map_eq, hYW.map_eq]