oxilean-std 0.1.2

//! Auto-generated module
//!
//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)

use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};

use super::types::{
    AbstractIntegral, BochnerIntegralApprox, Capacity, CaratheodoryExtension,
    ConditionalExpectation, ConvergenceTheoremType, DiscreteMeasure, DiscreteMeasureTyped,
    DiscreteProbabilitySpace, EgoroffData, FiniteSigmaAlgebra, FubiniData, HaarMeasureOnZpN,
    HausdorffDimensionEstimator, Independence, LebesgueMeasureEstimator, LpNormComputer, LusinData,
    Martingale, MeasureDisintExt, MeasureDisintegration, MonteCarloMeasureEstimator,
    RadonNikodymData, SignedMeasure,
};

pub fn app(f: Expr, a: Expr) -> Expr {
    Expr::App(Box::new(f), Box::new(a))
}
pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
    app(app(f, a), b)
}
pub fn cst(s: &str) -> Expr {
    Expr::Const(Name::str(s), vec![])
}
pub fn prop() -> Expr {
    Expr::Sort(Level::zero())
}
pub fn type0() -> Expr {
    Expr::Sort(Level::succ(Level::zero()))
}
pub fn pi(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
    Expr::Pi(bi, Name::str(name), Box::new(dom), Box::new(body))
}
pub fn arrow(a: Expr, b: Expr) -> Expr {
    pi(BinderInfo::Default, "_", a, b)
}
pub fn nat_ty() -> Expr {
    cst("Nat")
}
pub fn real_ty() -> Expr {
    cst("Real")
}
pub fn app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
    app(app2(f, a, b), c)
}
pub fn bvar(n: u32) -> Expr {
    Expr::BVar(n)
}
pub fn list_ty(elem: Expr) -> Expr {
    app(cst("List"), elem)
}
pub fn complex_ty() -> Expr {
    cst("Complex")
}
pub fn int_ty() -> Expr {
    cst("Int")
}
/// Sigma-algebra type: SigmaAlgebra (Ω : Type) : Type
pub fn sigma_algebra_ty() -> Expr {
    arrow(type0(), type0())
}
/// Measure type: Measure (Ω : Type) (F : SigmaAlgebra Ω) : Type
pub fn measure_ty() -> Expr {
    pi(
        BinderInfo::Default,
        "Omega",
        type0(),
        arrow(app(cst("SigmaAlgebra"), cst("Omega_bvar")), type0()),
    )
}
/// Probability space type: ProbabilitySpace (Ω : Type) : Prop
pub fn probability_space_ty() -> Expr {
    arrow(type0(), prop())
}
/// Measurable function type: MeasurableFunction (Ω E : Type) : Type
pub fn measurable_function_ty() -> Expr {
    pi(
        BinderInfo::Default,
        "Omega",
        type0(),
        arrow(type0(), type0()),
    )
}
/// Random variable type: RandomVariable (Ω : Type) : Type
pub fn random_variable_ty() -> Expr {
    arrow(type0(), type0())
}
/// Lebesgue integral type: LebesgueIntegral (f : Ω → Real) : Real
pub fn lebesgue_integral_ty() -> Expr {
    arrow(arrow(type0(), real_ty()), real_ty())
}
/// Monotone convergence theorem (Prop)
pub fn monotone_convergence_ty() -> Expr {
    prop()
}
/// Dominated convergence theorem (Prop)
pub fn dominated_convergence_ty() -> Expr {
    prop()
}
/// Fubini-Tonelli theorem (Prop)
pub fn fubini_tonelli_ty() -> Expr {
    prop()
}
/// Radon-Nikodym theorem: every σ-finite measure has a density w.r.t. another (Prop)
pub fn radon_nikodym_ty() -> Expr {
    prop()
}
/// Borel-Cantelli lemma:
///   First:  Σ P(Aₙ) < ∞ → P(lim sup Aₙ) = 0
///   Second: Σ P(Aₙ) = ∞, independent → P(lim sup Aₙ) = 1
pub fn borel_cantelli_ty() -> Expr {
    arrow(arrow(nat_ty(), real_ty()), prop())
}
/// Generated sigma-algebra: GeneratedSigmaAlgebra (Ω : Type) (C : Collection Ω) : SigmaAlgebra Ω
/// The smallest sigma-algebra containing a given collection C.
pub fn generated_sigma_algebra_ty() -> Expr {
    pi(
        BinderInfo::Default,
        "Omega",
        type0(),
        arrow(arrow(type0(), prop()), app(cst("SigmaAlgebra"), type0())),
    )
}
/// Borel sigma-algebra: BorelSigmaAlgebra (X : TopologicalSpace) : SigmaAlgebra X
/// Generated by the open sets of a topological space.
pub fn borel_sigma_algebra_ty() -> Expr {
    arrow(type0(), app(cst("SigmaAlgebra"), type0()))
}
/// Sigma-additivity: SigmaAdditive (μ : Measure Ω F) : Prop
/// μ(⋃ Aₙ) = Σ μ(Aₙ) for pairwise disjoint measurable sets.
pub fn sigma_additive_ty() -> Expr {
    arrow(type0(), prop())
}
/// Outer measure type: OuterMeasure (Ω : Type) : Type
/// A monotone, subadditive set function extending to all subsets.
pub fn outer_measure_ty() -> Expr {
    arrow(type0(), type0())
}
/// Carathéodory extension theorem: CaratheodoryExtension
/// Every pre-measure on a ring extends to a complete measure on the generated sigma-algebra.
pub fn caratheodory_extension_ty() -> Expr {
    prop()
}
/// Lebesgue translation invariance: LebesgueMeasure_TranslationInvariant : Prop
pub fn lebesgue_translation_invariant_ty() -> Expr {
    prop()
}
/// Lebesgue regularity: LebesgueMeasure_Regular : Prop
/// The Lebesgue measure is both inner and outer regular.
pub fn lebesgue_regularity_ty() -> Expr {
    prop()
}
/// Fatou's lemma: FatousLemma : (n → Ω → Real) → Prop
/// lim inf ∫ fₙ dμ ≤ ∫ lim inf fₙ dμ
pub fn fatous_lemma_ty() -> Expr {
    arrow(arrow(nat_ty(), arrow(type0(), real_ty())), prop())
}
/// Product measure type: ProductMeasure (Ω₁ Ω₂ : Type) : Type
pub fn product_measure_ty() -> Expr {
    pi(
        BinderInfo::Default,
        "Omega1",
        type0(),
        arrow(type0(), type0()),
    )
}
/// Signed measure type: SignedMeasure (Ω : Type) : Type
/// A measure that can take negative values (difference of two positive measures).
pub fn signed_measure_ty() -> Expr {
    arrow(type0(), type0())
}
/// Jordan decomposition: JordanDecomposition (ν : SignedMeasure Ω) : Prop
/// Every signed measure decomposes as ν = ν⁺ − ν⁻ where ν⁺, ν⁻ are positive measures.
pub fn jordan_decomposition_ty() -> Expr {
    arrow(arrow(type0(), real_ty()), prop())
}
/// Hahn decomposition: HahnDecomposition (ν : SignedMeasure Ω) : Prop
/// The space Ω decomposes into a positive set P and negative set N for ν.
pub fn hahn_decomposition_ty() -> Expr {
    arrow(type0(), prop())
}
/// Absolute continuity predicate: AbsolutelyContinuousOf (ν μ : Measure Ω) : Prop
/// ν ≪ μ: μ(A) = 0 implies ν(A) = 0.
pub fn absolutely_continuous_of_ty() -> Expr {
    arrow(type0(), arrow(type0(), prop()))
}
/// Lp space type: LpSpace (p : Real) (Ω : Type) : Type
/// Functions with finite p-th moment.
pub fn lp_space_ty() -> Expr {
    pi(BinderInfo::Default, "p", real_ty(), arrow(type0(), type0()))
}
/// Lp completeness: LpSpace_Complete (p : Real) : Prop
/// The Lp space is a Banach space (complete normed space).
pub fn lp_completeness_ty() -> Expr {
    arrow(real_ty(), prop())
}
/// Hölder's inequality: HoldersInequality (p q : Real) : Prop
/// ‖fg‖₁ ≤ ‖f‖_p · ‖g‖_q when 1/p + 1/q = 1.
pub fn holders_inequality_ty() -> Expr {
    arrow(real_ty(), arrow(real_ty(), prop()))
}
/// Minkowski's inequality: MinkowskisInequality (p : Real) : Prop
/// ‖f + g‖_p ≤ ‖f‖_p + ‖g‖_p for p ≥ 1.
pub fn minkowskis_inequality_ty() -> Expr {
    arrow(real_ty(), prop())
}
/// Riesz representation theorem for measures: RieszRepresentationMeasure (X : Type) : Prop
/// Positive linear functionals on C(X) correspond to regular Borel measures.
pub fn riesz_representation_measure_ty() -> Expr {
    arrow(type0(), prop())
}
/// Weak convergence of measures: WeakConvergence (μₙ μ : Measure Ω) : Prop
/// μₙ ⇀ μ: ∫ f dμₙ → ∫ f dμ for all bounded continuous f.
pub fn weak_convergence_measures_ty() -> Expr {
    arrow(arrow(nat_ty(), type0()), arrow(type0(), prop()))
}
/// Tightness of a sequence of measures: TightSequence (μₙ : n → Measure Ω) : Prop
/// For all ε > 0 there exists a compact K with μₙ(Kᶜ) < ε for all n.
pub fn tight_sequence_ty() -> Expr {
    arrow(arrow(nat_ty(), type0()), prop())
}
/// Prokhorov's theorem: ProkhorovTheorem : Prop
/// A tight sequence of probability measures has a weakly convergent subsequence.
pub fn prokhorov_theorem_ty() -> Expr {
    prop()
}
/// Regular conditional probability: RegularConditionalProbability (Ω E : Type) : Type
/// A kernel κ(ω, A) that serves as the conditional distribution given a sub-sigma-algebra.
pub fn regular_conditional_probability_ty() -> Expr {
    pi(
        BinderInfo::Default,
        "Omega",
        type0(),
        arrow(type0(), type0()),
    )
}
/// Disintegration of measures: DisintegrationOfMeasure (Ω E : Type) : Prop
/// A measure on a product space disintegrates as μ = ∫ μ_x dν(x).
pub fn disintegration_of_measure_ty() -> Expr {
    arrow(type0(), arrow(type0(), prop()))
}
/// Haar measure: HaarMeasure (G : Type) : Type
/// The unique (up to scalar) left-invariant regular Borel measure on a locally compact group.
pub fn haar_measure_ty() -> Expr {
    arrow(type0(), type0())
}
/// Haar measure uniqueness: HaarMeasure_Unique (G : Type) : Prop
pub fn haar_measure_unique_ty() -> Expr {
    arrow(type0(), prop())
}
/// Ergodic measure: ErgodicMeasure (Ω : Type) (T : Ω → Ω) : Prop
/// A T-invariant probability measure μ such that every T-invariant set has measure 0 or 1.
pub fn ergodic_measure_ty() -> Expr {
    pi(
        BinderInfo::Default,
        "Omega",
        type0(),
        arrow(arrow(type0(), type0()), prop()),
    )
}
/// Birkhoff ergodic theorem: BirkhoffErgodicTheorem : Prop
/// For ergodic T and integrable f, the time average converges to the space average a.e.
pub fn birkhoff_ergodic_theorem_ty() -> Expr {
    prop()
}
/// Optional stopping theorem: OptionalStoppingTheorem : Prop
/// For a martingale (Mₙ) and a bounded stopping time τ, E\[M_τ\] = E\[M₀\].
pub fn optional_stopping_theorem_ty() -> Expr {
    prop()
}
/// Conditional expectation type: ConditionalExpectation (Ω : Type) (G : SigmaAlgebra Ω) : Type
/// E[X | G] is the unique G-measurable function satisfying ∫_A E[X|G] dμ = ∫_A X dμ for all A ∈ G.
pub fn conditional_expectation_ty() -> Expr {
    pi(
        BinderInfo::Default,
        "Omega",
        type0(),
        arrow(
            app(cst("SigmaAlgebra"), type0()),
            arrow(arrow(type0(), real_ty()), arrow(type0(), real_ty())),
        ),
    )
}
/// Gaussian measure type: GaussianMeasure (H : HilbertSpace) : Type
/// A measure on a Hilbert space determined by mean m and covariance operator C.
pub fn gaussian_measure_ty() -> Expr {
    arrow(type0(), type0())
}
/// Wiener measure: WienerMeasure : Type
/// The unique probability measure on C(\[0,1\]) representing standard Brownian motion.
pub fn wiener_measure_ty() -> Expr {
    type0()
}
/// Hausdorff measure type: HausdorffMeasure (d : Real) (X : MetricSpace) : Type
/// The d-dimensional Hausdorff measure on a metric space.
pub fn hausdorff_measure_ty() -> Expr {
    pi(BinderInfo::Default, "d", real_ty(), arrow(type0(), type0()))
}
/// Hausdorff dimension: HausdorffDimension (X : MetricSpace) : Real
/// inf { d : ℝ≥0 | H^d(X) = 0 }.
pub fn hausdorff_dimension_ty() -> Expr {
    arrow(type0(), real_ty())
}
/// Martingale type: Martingale (Ω : Type) (n : Nat) : Type
/// An adapted integrable process (Mₙ) satisfying E[M_{n+1} | Fₙ] = Mₙ a.s.
pub fn martingale_ty() -> Expr {
    pi(
        BinderInfo::Default,
        "Omega",
        type0(),
        arrow(nat_ty(), type0()),
    )
}
/// Stopping time type: StoppingTime (Ω : Type) : Type
/// A measurable random variable τ : Ω → ℕ ∪ {∞} adapted to a filtration.
pub fn stopping_time_ty() -> Expr {
    arrow(type0(), arrow(nat_ty(), prop()))
}
/// Doob's upcrossing inequality: DoobUpcrossingInequality : Prop
pub fn doob_upcrossing_inequality_ty() -> Expr {
    prop()
}
/// Martingale convergence theorem: MartingaleConvergenceTheorem : Prop
/// An L¹-bounded martingale converges a.s.
pub fn martingale_convergence_ty() -> Expr {
    prop()
}
/// Carathéodory extension theorem type: CaratheodoryExtensionFull : Prop
/// A pre-measure on a ring of sets extends uniquely to a complete measure on
/// the generated sigma-algebra. This is the foundational existence theorem.
pub fn caratheodory_extension_full_ty() -> Expr {
    prop()
}
/// Hahn decomposition theorem: HahnDecompositionFull : Prop
/// Every signed measure has a positive set P and negative set N such that Ω = P ∪ N.
pub fn hahn_decomposition_full_ty() -> Expr {
    prop()
}
/// Jordan decomposition full: JordanDecompositionFull : Prop
/// The Jordan decomposition ν = ν⁺ − ν⁻ is unique (minimal decomposition).
pub fn jordan_decomposition_full_ty() -> Expr {
    prop()
}
/// Total variation measure: TotalVariation (ν : SignedMeasure Ω) : Real
/// |ν|(A) = ν⁺(A) + ν⁻(A); the total variation of the signed measure.
pub fn total_variation_ty() -> Expr {
    arrow(arrow(type0(), real_ty()), real_ty())
}
/// Banach lattice of measures: BanachLatticeMeasures (Ω : Type) : Type
/// The space of signed measures with total variation norm forms a Banach lattice.
pub fn banach_lattice_measures_ty() -> Expr {
    arrow(type0(), type0())
}
/// Bochner integral: BochnerIntegral (Ω E : Type) : Type
/// The Bochner integral extends Lebesgue integration to Banach-space-valued functions.
pub fn bochner_integral_ty() -> Expr {
    pi(
        BinderInfo::Default,
        "Omega",
        type0(),
        arrow(type0(), type0()),
    )
}
/// Bochner integrability: BochnerIntegrable (f : Ω → E) : Prop
/// A Banach-valued function is Bochner integrable iff it is strongly measurable
/// and ‖f‖ is Lebesgue integrable.
pub fn bochner_integrable_ty() -> Expr {
    arrow(arrow(type0(), type0()), prop())
}
/// Pettis integral: PettisIntegral (Ω E : Type) : Type
/// The Pettis integral (weak integral): ⟨∫f dμ, x*⟩ = ∫⟨f, x*⟩ dμ for all x* ∈ E*.
pub fn pettis_integral_ty() -> Expr {
    pi(
        BinderInfo::Default,
        "Omega",
        type0(),
        arrow(type0(), type0()),
    )
}
/// Dunford integral: DunfordIntegral (Ω E : Type) : Type
/// The Dunford integral (weakest integral): x**(∫f dμ) = ∫x*(f) dμ for x** ∈ E**.
pub fn dunford_integral_ty() -> Expr {
    pi(
        BinderInfo::Default,
        "Omega",
        type0(),
        arrow(type0(), type0()),
    )
}
/// Lp duality: LpDuality (p q : Real) : Prop
/// (Lᵖ)* = Lq when 1/p + 1/q = 1, 1 < p < ∞.
pub fn lp_duality_ty() -> Expr {
    arrow(real_ty(), arrow(real_ty(), prop()))
}
/// Characteristic function (Fourier transform of a measure):
/// CharacteristicFunction (μ : ProbabilityMeasure Ω) : ℝⁿ → ℂ
pub fn characteristic_function_ty() -> Expr {
    arrow(type0(), arrow(real_ty(), complex_ty()))
}
/// Lévy continuity theorem: LevyContinuityTheorem : Prop
/// A sequence of probability measures converges weakly iff their characteristic
/// functions converge pointwise to a continuous function.
pub fn levy_continuity_theorem_ty() -> Expr {
    prop()
}
/// Prokhorov metric: ProkhorovMetric (Ω : Type) : Real
/// The Prokhorov metric metrizes weak convergence on probability measures.
pub fn prokhorov_metric_ty() -> Expr {
    arrow(type0(), arrow(type0(), real_ty()))
}
/// Self-similar measure: SelfSimilarMeasure (d : Real) : Type
/// A measure satisfying a self-similarity equation: μ = Σᵢ pᵢ · μ ∘ Sᵢ⁻¹.
pub fn self_similar_measure_ty() -> Expr {
    arrow(real_ty(), type0())
}
/// Moran's theorem: MoranTheorem : Prop
/// Under the open set condition, the Hausdorff dimension of a self-similar set
/// is the unique solution to Σᵢ rᵢˢ = 1.
pub fn moran_theorem_ty() -> Expr {
    prop()
}
/// Covering dimension: CoveringDimension (X : MetricSpace) : Nat
/// The box-counting (Minkowski) dimension of a metric space.
pub fn covering_dimension_ty() -> Expr {
    arrow(type0(), nat_ty())
}
/// Rectifiable set: RectifiableSet (n k : Nat) : Type
/// A set in ℝⁿ that is (countably) k-rectifiable: covered by a countable
/// union of images of Lipschitz maps from ℝᵏ.
pub fn rectifiable_set_ty() -> Expr {
    arrow(nat_ty(), arrow(nat_ty(), type0()))
}
/// Varifold: Varifold (n k : Nat) : Type
/// A generalised surface in ℝⁿ (Radon measure on Grassmannian bundle).
pub fn varifold_ty() -> Expr {
    arrow(nat_ty(), arrow(nat_ty(), type0()))
}
/// Current: Current (n k : Nat) : Type
/// A de Rham current = continuous linear functional on compactly supported k-forms.
pub fn current_ty() -> Expr {
    arrow(nat_ty(), arrow(nat_ty(), type0()))
}
/// Federer-Fleming closure theorem: FedererFlemingClosure : Prop
/// The closure of the class of integral currents under weak convergence.
pub fn federer_fleming_closure_ty() -> Expr {
    prop()
}
/// Invariant measure existence: InvariantMeasureExistence (T : Ω → Ω) : Prop
/// Krylov-Bogolyubov theorem: every continuous map on a compact metric space
/// has an invariant probability measure.
pub fn invariant_measure_existence_ty() -> Expr {
    arrow(arrow(type0(), type0()), prop())
}
/// Ergodic decomposition theorem: ErgodicDecompositionTheorem : Prop
/// Every T-invariant probability measure decomposes as an integral of ergodic measures.
pub fn ergodic_decomposition_theorem_ty() -> Expr {
    prop()
}
/// Poincaré recurrence theorem: PoincareRecurrenceTheorem : Prop
/// For a measure-preserving system on a finite measure space, μ-almost every
/// point returns to any positive-measure set infinitely often.
pub fn poincare_recurrence_theorem_ty() -> Expr {
    prop()
}
/// Positive operator-valued measure (POVM): POVM (H : HilbertSpace) : Type
/// A POVM is a measure taking values in positive semidefinite operators on H,
/// summing to the identity. Foundation of quantum measurement theory.
pub fn povm_ty() -> Expr {
    arrow(type0(), type0())
}
/// Quantum state: QuantumState (H : HilbertSpace) : Type
/// A density matrix (positive semidefinite trace-1 operator on H).
pub fn quantum_state_ty() -> Expr {
    arrow(type0(), type0())
}
/// Born rule: BornRule (M : POVM H) (ρ : QuantumState H) : Prop
/// Probability of outcome m is tr(ρ Mₘ).
pub fn born_rule_ty() -> Expr {
    arrow(type0(), arrow(type0(), prop()))
}
/// Choquet simplex: ChoquetSimplex (K : ConvexSet) : Prop
/// K is a Choquet simplex if every point has a unique representing measure
/// supported on extreme points.
pub fn choquet_simplex_ty() -> Expr {
    arrow(type0(), prop())
}
/// Choquet integral representation: ChoquetIntegralRepresentation (K : ConvexSet) : Prop
/// Every element of a compact convex set K is represented by a probability measure
/// supported on the extreme points (Krein-Milman + Choquet).
pub fn choquet_integral_representation_ty() -> Expr {
    arrow(type0(), prop())
}
/// Rokhlin disintegration theorem: RokhlinDisintegration (Ω B : Type) : Prop
/// A measure-preserving map T : Ω → B admits a disintegration μ = ∫_B μ_b dν(b).
pub fn rokhlin_disintegration_ty() -> Expr {
    arrow(type0(), arrow(type0(), prop()))
}
/// State on a C*-algebra: StateOnCStarAlgebra (A : CStarAlgebra) : Type
/// A positive linear functional φ : A → ℂ with φ(1) = 1; non-commutative probability.
pub fn state_on_cstar_algebra_ty() -> Expr {
    arrow(type0(), type0())
}
/// GNS construction: GNSConstruction (A : CStarAlgebra) (φ : State A) : Prop
/// Every state on a C*-algebra arises from a cyclic representation (Gelfand-Naimark-Segal).
pub fn gns_construction_ty() -> Expr {
    arrow(type0(), arrow(type0(), prop()))
}
/// Von Neumann algebra: VonNeumannAlgebra (H : HilbertSpace) : Type
/// A *-subalgebra of B(H) closed in the weak operator topology; carries a
/// canonical normal faithful state in the finite case.
pub fn von_neumann_algebra_ty() -> Expr {
    arrow(type0(), type0())
}
/// Murray-von Neumann equivalence: MurrayVonNeumannEquiv (A : VonNeumannAlgebra) : Prop
/// Two projections are equivalent if they are related by a partial isometry in A.
pub fn murray_von_neumann_equiv_ty() -> Expr {
    arrow(type0(), prop())
}
pub fn build_measure_theory_env(env: &mut Environment) {
    let axioms: &[(&str, Expr)] = &[
        ("SigmaAlgebra", sigma_algebra_ty()),
        ("Measure", measure_ty()),
        ("ProbabilitySpace", probability_space_ty()),
        ("MeasurableFunction", measurable_function_ty()),
        ("RandomVariable", random_variable_ty()),
        ("LebesgueIntegral", lebesgue_integral_ty()),
        ("monotone_convergence", monotone_convergence_ty()),
        ("dominated_convergence", dominated_convergence_ty()),
        ("fubini_tonelli", fubini_tonelli_ty()),
        ("radon_nikodym", radon_nikodym_ty()),
        ("borel_cantelli", borel_cantelli_ty()),
        ("SigmaFinite", arrow(type0(), prop())),
        (
            "AbsolutelyContinuous",
            arrow(type0(), arrow(type0(), prop())),
        ),
        ("AlmostEverywhere", arrow(arrow(type0(), prop()), prop())),
        ("Integrable", arrow(arrow(type0(), real_ty()), prop())),
        ("Expectation", arrow(arrow(type0(), real_ty()), real_ty())),
        ("Variance", arrow(arrow(type0(), real_ty()), real_ty())),
        ("SigmaAlgebraMem", arrow(list_ty(nat_ty()), prop())),
        ("GeneratedSigmaAlgebra", generated_sigma_algebra_ty()),
        ("BorelSigmaAlgebra", borel_sigma_algebra_ty()),
        ("SigmaAdditive", sigma_additive_ty()),
        ("OuterMeasure", outer_measure_ty()),
        ("caratheodory_extension", caratheodory_extension_ty()),
        (
            "lebesgue_translation_invariant",
            lebesgue_translation_invariant_ty(),
        ),
        ("lebesgue_regularity", lebesgue_regularity_ty()),
        ("fatous_lemma", fatous_lemma_ty()),
        ("ProductMeasure", product_measure_ty()),
        ("SignedMeasure", signed_measure_ty()),
        ("jordan_decomposition", jordan_decomposition_ty()),
        ("hahn_decomposition", hahn_decomposition_ty()),
        ("AbsolutelyContinuousOf", absolutely_continuous_of_ty()),
        ("LpSpace", lp_space_ty()),
        ("lp_completeness", lp_completeness_ty()),
        ("holders_inequality", holders_inequality_ty()),
        ("minkowskis_inequality", minkowskis_inequality_ty()),
        (
            "riesz_representation_measure",
            riesz_representation_measure_ty(),
        ),
        ("WeakConvergenceMeasures", weak_convergence_measures_ty()),
        ("TightSequence", tight_sequence_ty()),
        ("prokhorov_theorem", prokhorov_theorem_ty()),
        (
            "RegularConditionalProbability",
            regular_conditional_probability_ty(),
        ),
        ("disintegration_of_measure", disintegration_of_measure_ty()),
        ("HaarMeasure", haar_measure_ty()),
        ("haar_measure_unique", haar_measure_unique_ty()),
        ("ErgodicMeasure", ergodic_measure_ty()),
        ("birkhoff_ergodic_theorem", birkhoff_ergodic_theorem_ty()),
        ("Martingale", martingale_ty()),
        ("StoppingTime", stopping_time_ty()),
        ("optional_stopping_theorem", optional_stopping_theorem_ty()),
        (
            "doob_upcrossing_inequality",
            doob_upcrossing_inequality_ty(),
        ),
        ("martingale_convergence", martingale_convergence_ty()),
        ("ConditionalExpectation", conditional_expectation_ty()),
        ("GaussianMeasure", gaussian_measure_ty()),
        ("WienerMeasure", wiener_measure_ty()),
        ("HausdorffMeasure", hausdorff_measure_ty()),
        ("HausdorffDimension", hausdorff_dimension_ty()),
        (
            "caratheodory_extension_full",
            caratheodory_extension_full_ty(),
        ),
        ("hahn_decomposition_full", hahn_decomposition_full_ty()),
        ("jordan_decomposition_full", jordan_decomposition_full_ty()),
        ("TotalVariation", total_variation_ty()),
        ("BanachLatticeMeasures", banach_lattice_measures_ty()),
        ("BochnerIntegral", bochner_integral_ty()),
        ("BochnerIntegrable", bochner_integrable_ty()),
        ("PettisIntegral", pettis_integral_ty()),
        ("DunfordIntegral", dunford_integral_ty()),
        ("lp_duality", lp_duality_ty()),
        ("CharacteristicFunction", characteristic_function_ty()),
        ("levy_continuity_theorem", levy_continuity_theorem_ty()),
        ("ProkhorovMetric", prokhorov_metric_ty()),
        ("SelfSimilarMeasure", self_similar_measure_ty()),
        ("moran_theorem", moran_theorem_ty()),
        ("CoveringDimension", covering_dimension_ty()),
        ("RectifiableSet", rectifiable_set_ty()),
        ("Varifold", varifold_ty()),
        ("Current", current_ty()),
        ("federer_fleming_closure", federer_fleming_closure_ty()),
        (
            "invariant_measure_existence",
            invariant_measure_existence_ty(),
        ),
        (
            "ergodic_decomposition_theorem",
            ergodic_decomposition_theorem_ty(),
        ),
        (
            "poincare_recurrence_theorem",
            poincare_recurrence_theorem_ty(),
        ),
        ("POVM", povm_ty()),
        ("QuantumState", quantum_state_ty()),
        ("born_rule", born_rule_ty()),
        ("ChoquetSimplex", choquet_simplex_ty()),
        (
            "choquet_integral_representation",
            choquet_integral_representation_ty(),
        ),
        ("rokhlin_disintegration", rokhlin_disintegration_ty()),
        ("StateOnCStarAlgebra", state_on_cstar_algebra_ty()),
        ("gns_construction", gns_construction_ty()),
        ("VonNeumannAlgebra", von_neumann_algebra_ty()),
        ("murray_von_neumann_equiv", murray_von_neumann_equiv_ty()),
    ];
    for (name, ty) in axioms {
        env.add(Declaration::Axiom {
            name: Name::str(*name),
            univ_params: vec![],
            ty: ty.clone(),
        })
        .ok();
    }
}
/// Discrete Lebesgue integral: ∫ f dμ = Σᵢ f(i) · μ({i}).
pub fn discrete_integral(f: &[f64], measure: &DiscreteMeasure) -> f64 {
    f.iter()
        .zip(measure.weights.iter())
        .map(|(fi, wi)| fi * wi)
        .sum()
}
/// Expectation E[g(X)] over a discrete probability space.
///
/// Computes Σₒ g(outcome_o) · P(outcome_o).
pub fn expectation(f: &dyn Fn(&str) -> f64, space: &DiscreteProbabilitySpace) -> f64 {
    space
        .outcomes
        .iter()
        .zip(space.probabilities.iter())
        .map(|(o, p)| f(o.as_str()) * p)
        .sum()
}
#[cfg(test)]
mod tests {
    use super::*;
    #[test]
    fn test_discrete_prob_space_uniform() {
        let space = DiscreteProbabilitySpace::uniform(vec!["H".to_string(), "T".to_string()]);
        assert_eq!(space.n_outcomes(), 2);
        assert!(space.is_valid());
        assert!((space.prob("H") - 0.5).abs() < 1e-10);
        assert!((space.prob("T") - 0.5).abs() < 1e-10);
    }
    #[test]
    fn test_discrete_prob_space_prob() {
        let space = DiscreteProbabilitySpace::new(
            vec!["a".to_string(), "b".to_string(), "c".to_string()],
            vec![0.2, 0.5, 0.3],
        )
        .expect("should be valid");
        assert!((space.prob("a") - 0.2).abs() < 1e-10);
        assert!((space.prob("b") - 0.5).abs() < 1e-10);
        assert!((space.prob("c") - 0.3).abs() < 1e-10);
        assert_eq!(space.prob("d"), 0.0);
    }
    #[test]
    fn test_discrete_prob_invalid() {
        let result =
            DiscreteProbabilitySpace::new(vec!["a".to_string(), "b".to_string()], vec![0.3, 0.3]);
        assert!(result.is_none(), "Should be None when probs don't sum to 1");
    }
    #[test]
    fn test_finite_sigma_algebra_trivial() {
        let sa = FiniteSigmaAlgebra::trivial(4);
        assert_eq!(sa.sets.len(), 2);
        assert!(sa.is_sigma_algebra());
    }
    #[test]
    fn test_finite_sigma_algebra_power_set_is_valid() {
        let sa = FiniteSigmaAlgebra::power_set(3);
        assert_eq!(sa.sets.len(), 8);
        assert!(sa.is_sigma_algebra());
    }
    #[test]
    fn test_discrete_measure_counting() {
        let m = DiscreteMeasure::counting_measure(5);
        assert_eq!(m.n_elements, 5);
        assert!((m.measure_of(&[0, 2, 4]) - 3.0).abs() < 1e-10);
        assert!(!m.is_probability());
    }
    #[test]
    fn test_discrete_integral() {
        let m = DiscreteMeasure::new(vec![0.5, 0.3, 0.2]);
        let f = vec![1.0, 2.0, 3.0];
        let result = discrete_integral(&f, &m);
        assert!((result - 1.7).abs() < 1e-10, "Expected 1.7, got {}", result);
    }
    #[test]
    fn test_expectation() {
        let space = DiscreteProbabilitySpace::uniform(vec!["H".to_string(), "T".to_string()]);
        let e = expectation(&|o| if o == "H" { 1.0 } else { 0.0 }, &space);
        assert!((e - 0.5).abs() < 1e-10, "Expected 0.5, got {}", e);
    }
    #[test]
    fn test_build_measure_theory_env() {
        let mut env = Environment::new();
        build_measure_theory_env(&mut env);
        assert!(!env.is_empty());
    }
    #[test]
    fn test_discrete_measure_typed_integrate() {
        let m = DiscreteMeasureTyped::new(vec![1u32, 2, 3], vec![0.5, 0.3, 0.2]);
        let result = m.integrate(|&x| x as f64);
        assert!((result - 1.7).abs() < 1e-10);
    }
    #[test]
    fn test_discrete_measure_typed_normalize() {
        let m = DiscreteMeasureTyped::new(vec!["a", "b"], vec![2.0, 3.0]);
        let nm = m.normalize().expect("non-zero total");
        assert!((nm.total_mass() - 1.0).abs() < 1e-10);
        assert!((nm.atom_weight(&"a").expect("atom_weight should succeed") - 0.4).abs() < 1e-10);
    }
    #[test]
    fn test_discrete_measure_typed_push_forward() {
        let m = DiscreteMeasureTyped::new(vec![0usize, 1, 2, 3], vec![0.25, 0.25, 0.25, 0.25]);
        let pf = m.push_forward(|&x| if x % 2 == 0 { "even" } else { "odd" });
        let even_w = pf.atom_weight(&"even").expect("atom_weight should succeed");
        let odd_w = pf.atom_weight(&"odd").expect("atom_weight should succeed");
        assert!((even_w - 0.5).abs() < 1e-10);
        assert!((odd_w - 0.5).abs() < 1e-10);
    }
    #[test]
    fn test_lebesgue_estimator_full_interval() {
        let est = LebesgueMeasureEstimator::new(0.0, 1.0, 10_000);
        let m = est.estimate(&[(0.0, 1.0)]);
        assert!((m - 1.0).abs() < 1e-3);
    }
    #[test]
    fn test_lebesgue_estimator_half() {
        let est = LebesgueMeasureEstimator::new(0.0, 1.0, 100_000);
        let m = est.estimate(&[(0.0, 0.5)]);
        assert!((m - 0.5).abs() < 1e-3);
    }
    #[test]
    fn test_lp_norm_l2() {
        let lp = LpNormComputer::uniform(4);
        let f = vec![1.0, 2.0, 3.0, 4.0];
        let expected = (7.5_f64).sqrt();
        let got = lp.lp_norm(&f, 2.0);
        assert!((got - expected).abs() < 1e-10);
    }
    #[test]
    fn test_holder_inequality() {
        let lp = LpNormComputer::uniform(4);
        let f = vec![1.0, 0.0, 2.0, 1.0];
        let g = vec![2.0, 3.0, 0.0, 1.0];
        let (lhs, rhs, holds) = lp.verify_holder(&f, &g, 2.0);
        assert!(holds, "Hölder failed: lhs={} rhs={}", lhs, rhs);
    }
    #[test]
    fn test_minkowski_inequality() {
        let lp = LpNormComputer::uniform(4);
        let f = vec![1.0, 2.0, 0.0, 1.0];
        let g = vec![0.0, 1.0, 3.0, 1.0];
        let (lhs, rhs, holds) = lp.verify_minkowski(&f, &g, 2.0);
        assert!(holds, "Minkowski failed: lhs={} rhs={}", lhs, rhs);
    }
    #[test]
    fn test_monte_carlo_estimator_circle() {
        let est = MonteCarloMeasureEstimator::new(10_000, 2);
        let area = est.estimate_unit_cube(|pt| {
            let x = pt[0];
            let y = pt[1];
            x * x + y * y <= 1.0
        });
        let pi_over_4 = std::f64::consts::PI / 4.0;
        assert!((area - pi_over_4).abs() < 0.02, "got {}", area);
    }
    #[test]
    fn test_haar_measure_zn_atom_weight() {
        let h = HaarMeasureOnZpN::new(6);
        assert!((h.atom_weight() - 1.0 / 6.0).abs() < 1e-12);
    }
    #[test]
    fn test_haar_measure_zn_translation_invariance() {
        let h = HaarMeasureOnZpN::new(8);
        let set = vec![0usize, 2, 4, 6];
        assert!(h.verify_translation_invariance(&set));
    }
    #[test]
    fn test_haar_measure_zn_integrate_constant() {
        let h = HaarMeasureOnZpN::new(5);
        let result = h.integrate(|_| 1.0);
        assert!((result - 1.0).abs() < 1e-12);
    }
    #[test]
    fn test_haar_measure_zn_convolve_delta() {
        let n = 4usize;
        let h = HaarMeasureOnZpN::new(n);
        let f = vec![1.0, 2.0, 3.0, 4.0];
        let delta = [1.0, 0.0, 0.0, 0.0];
        let conv = h.convolve(&f, &delta);
        for i in 0..n {
            assert!((conv[i] - f[i] / n as f64).abs() < 1e-12);
        }
    }
    #[test]
    fn test_build_env_has_new_axioms() {
        let mut env = Environment::new();
        build_measure_theory_env(&mut env);
        for name in &[
            "GeneratedSigmaAlgebra",
            "BorelSigmaAlgebra",
            "OuterMeasure",
            "SignedMeasure",
            "LpSpace",
            "HaarMeasure",
            "ErgodicMeasure",
            "Martingale",
            "ConditionalExpectation",
            "WienerMeasure",
            "HausdorffMeasure",
        ] {
            assert!(env.contains(&Name::str(*name)), "Missing axiom: {}", name);
        }
    }
    #[test]
    fn test_caratheodory_extension_total_mass() {
        let ext = CaratheodoryExtension::new(vec![0.25, 0.25, 0.25, 0.25]);
        assert!((ext.total_mass() - 1.0).abs() < 1e-12);
    }
    #[test]
    fn test_caratheodory_extension_additive() {
        let ext = CaratheodoryExtension::new(vec![0.1, 0.2, 0.3, 0.4]);
        assert!(ext.is_finitely_additive(&[0, 1], &[2, 3]));
        assert!(!ext.is_finitely_additive(&[0, 1], &[1, 2]));
    }
    #[test]
    fn test_caratheodory_extension_measurability() {
        let ext = CaratheodoryExtension::new(vec![0.1, 0.2, 0.3, 0.4]);
        assert!(ext.is_caratheodory_measurable(&[0]));
        assert!(ext.is_caratheodory_measurable(&[0, 1, 2, 3]));
    }
    #[test]
    fn test_bochner_integral_constant() {
        let approx = BochnerIntegralApprox::new(vec![0.5, 0.5], 2);
        let values = vec![vec![1.0, 2.0], vec![1.0, 2.0]];
        let result = approx.integrate(&values);
        assert!((result[0] - 1.0).abs() < 1e-12);
        assert!((result[1] - 2.0).abs() < 1e-12);
    }
    #[test]
    fn test_bochner_integral_jensen() {
        let approx = BochnerIntegralApprox::new(vec![0.3, 0.7], 2);
        let values = vec![vec![1.0, 0.0], vec![0.0, 1.0]];
        assert!(approx.verify_jensen(&values));
    }
    #[test]
    fn test_measure_disintegration_marginal() {
        let disint = MeasureDisintegration::new(vec![0.2, 0.3, 0.1, 0.4], vec![0, 0, 1, 1], 2);
        let nu = disint.marginal();
        assert!((nu[0] - 0.5).abs() < 1e-12);
        assert!((nu[1] - 0.5).abs() < 1e-12);
    }
    #[test]
    fn test_measure_disintegration_identity() {
        let disint = MeasureDisintegration::new(vec![0.2, 0.3, 0.1, 0.4], vec![0, 0, 1, 1], 2);
        let f = vec![1.0, 2.0, 3.0, 4.0];
        let (lhs, rhs, holds) = disint.verify_disintegration(&f);
        assert!(holds, "Disintegration: lhs={} rhs={}", lhs, rhs);
    }
    #[test]
    fn test_hausdorff_box_count_line() {
        let pts = vec![(0.0, 0.0), (0.25, 0.0), (0.5, 0.0), (0.75, 0.0)];
        let est = HausdorffDimensionEstimator::new(pts);
        assert_eq!(est.box_count(0.5), 2);
        assert_eq!(est.box_count(0.25), 4);
    }
    #[test]
    fn test_hausdorff_dimension_full_square() {
        // Use a 64x64 grid over [0,1]² for accurate box-counting dimension estimate
        let n = 64;
        let pts: Vec<(f64, f64)> = (0..n)
            .flat_map(|i| {
                (0..n).map(move |j| (i as f64 / (n - 1) as f64, j as f64 / (n - 1) as f64))
            })
            .collect();
        let est = HausdorffDimensionEstimator::new(pts);
        let dim = est.estimate_dimension(5);
        assert!(dim > 1.5 && dim < 2.5, "Expected dim ≈ 2, got {}", dim);
    }
    #[test]
    fn test_build_env_has_extended_axioms() {
        let mut env = Environment::new();
        build_measure_theory_env(&mut env);
        for name in &[
            "BochnerIntegral",
            "POVM",
            "QuantumState",
            "VonNeumannAlgebra",
            "ChoquetSimplex",
            "Varifold",
            "Current",
            "RectifiableSet",
            "SelfSimilarMeasure",
        ] {
            assert!(
                env.contains(&Name::str(*name)),
                "Missing extended axiom: {}",
                name
            );
        }
    }
}
#[cfg(test)]
mod extended_measure_tests {
    use super::*;
    #[test]
    fn test_signed_measure() {
        let sm = SignedMeasure::jordan("P", "N", 3.0);
        assert!(sm.is_positive());
        assert!(sm.hahn_decomposition().contains("P=P"));
    }
    #[test]
    fn test_abstract_integral() {
        let leb = AbstractIntegral::lebesgue("R");
        assert!(leb.is_lebesgue);
        assert!(leb.description().contains("Lebesgue"));
    }
    #[test]
    fn test_martingale() {
        let mg = Martingale::true_martingale("F_t");
        assert!(!mg.is_sub);
        assert!(mg.optional_stopping_applies(true));
        assert!(!mg.optional_stopping_applies(false));
    }
    #[test]
    fn test_fubini() {
        let f = FubiniData::fubini("X", "Y");
        assert!(f.can_interchange());
    }
    #[test]
    fn test_convergence_theorems() {
        let dct = ConvergenceTheoremType::DominatedConvergence;
        assert_eq!(dct.name(), "DCT");
        let mct = ConvergenceTheoremType::MonotoneConvergence;
        assert_eq!(mct.name(), "MCT");
    }
    #[test]
    fn test_radon_nikodym() {
        let rn = RadonNikodymData::new("nu", "mu");
        assert!(rn.derivative_exists());
        assert!(rn.density_name.contains("dnu"));
    }
    #[test]
    fn test_disintegration() {
        let d = MeasureDisintExt::standard("X", "Y");
        assert!(d.rokhlin_applies());
    }
}
#[cfg(test)]
mod extended_measure_tests2 {
    use super::*;
    #[test]
    fn test_capacity() {
        let cap = Capacity::newtonian();
        assert!(cap.is_submodular);
        assert!(cap.is_measure());
        assert!(cap.choquet_integral_description().contains("Choquet"));
    }
    #[test]
    fn test_lusin() {
        let l = LusinData::new("R", "f", 0.01);
        let desc = l.compact_set_description();
        assert!(desc.contains("μ(K)"));
    }
    #[test]
    fn test_egoroff() {
        let e = EgoroffData::new("f_n", "f", 1.0);
        assert!(e.description().contains("Egoroff"));
    }
    #[test]
    fn test_independence() {
        let ind = Independence::new(
            vec!["A".to_string(), "B".to_string(), "C".to_string()],
            true,
        );
        assert!(ind.mutually_independent_implies_pairwise());
        assert_eq!(ind.count(), 3);
    }
    #[test]
    fn test_conditional_expectation() {
        let ce = ConditionalExpectation::new("X", "G");
        assert!(ce.is_tower_property);
        assert!(ce.tower_description().contains("tower") || ce.tower_description().contains("E["));
    }
}