def Approximation.IsApprox {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Q' : Ω → ℝ) (Q ε δ : ℝ) : Prop

def Approximation.IsPolyTime (runtime : ℕ → ℝ → ℝ → ℕ) : Prop

structure Approximation.FPRAS : Type (u_1 + 1)

• Ω : ℕ → ℝ → ℝ → Type u_1
• meas (n : ℕ) (ε δ : ℝ) : MeasurableSpace (self.Ω n ε δ)
• μ (n : ℕ) (ε δ : ℝ) : MeasureTheory.Measure (self.Ω n ε δ)
• Q : ℕ → ℝ
• estimator (n : ℕ) (ε δ : ℝ) : self.Ω n ε δ → ℝ
• runtime : ℕ → ℝ → ℝ → ℕ
• approx (n : ℕ) (ε δ : ℝ) : 0 < ε → 0 < δ → IsApprox (self.μ n ε δ) (self.estimator n ε δ) (self.Q n) ε δ
• poly_time : IsPolyTime self.runtime