| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1105 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (251 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (375 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (18 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (79 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (39 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (306 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |
Global Index
A
adjunction_counit [lemma, in QBS.measure_qbs_adjunction]adjunction_unit [lemma, in QBS.measure_qbs_adjunction]
as_qbs_prob_recover_full [lemma, in QBS.measure_as_qbs_measure]
as_qbs_prob_recover [lemma, in QBS.measure_as_qbs_measure]
as_qbs_prob [definition, in QBS.measure_as_qbs_measure]
B
bayesian_regression.d_pair_meas_tac [variable, in QBS.showcase.bayesian_regression]bayesian_regression.phase1_sigma5 [variable, in QBS.showcase.bayesian_regression]
bayesian_regression.phase1_mu5 [variable, in QBS.showcase.bayesian_regression]
bayesian_regression.noise_sigma [variable, in QBS.showcase.bayesian_regression]
bayesian_regression.prior_sigma [variable, in QBS.showcase.bayesian_regression]
bayesian_regression.R [variable, in QBS.showcase.bayesian_regression]
bayesian_regression [section, in QBS.showcase.bayesian_regression]
bayesian_regression [library]
binary_digit_interleaving.composed_bijection [section, in QBS.standard_borel]
binary_digit_interleaving.measurability_constructions.step [variable, in QBS.standard_borel]
binary_digit_interleaving.measurability_constructions [section, in QBS.standard_borel]
binary_digit_interleaving.round_trips [section, in QBS.standard_borel]
binary_digit_interleaving.pairing_reconstruction [section, in QBS.standard_borel]
binary_digit_interleaving.binary_digit_arithmetic [section, in QBS.standard_borel]
binary_digit_interleaving.R [variable, in QBS.standard_borel]
binary_digit_interleaving [section, in QBS.standard_borel]
bin_sum_has_one_gt0 [lemma, in QBS.standard_borel]
bin_digit_iter [lemma, in QBS.standard_borel]
bin_digits_bin_sum [lemma, in QBS.standard_borel]
bin_sum_shift [lemma, in QBS.standard_borel]
bin_sum_no_trailing_lt1 [lemma, in QBS.standard_borel]
bin_digits_no_trailing_ones [lemma, in QBS.standard_borel]
bin_sum_ext [lemma, in QBS.standard_borel]
bin_digits_reconstruction [lemma, in QBS.standard_borel]
bin_sum_ge0 [lemma, in QBS.standard_borel]
bin_sum_le1 [lemma, in QBS.standard_borel]
bin_partial_sum_nd [lemma, in QBS.standard_borel]
bin_partial_sum_ge0 [lemma, in QBS.standard_borel]
bin_partial_sum_le1 [lemma, in QBS.standard_borel]
bin_digits [definition, in QBS.standard_borel]
bin_sum [definition, in QBS.standard_borel]
bin_partial_sum [definition, in QBS.standard_borel]
bin_digit [definition, in QBS.standard_borel]
boolQ [definition, in QBS.quasi_borel]
bool_standard_borel [lemma, in QBS.measure_qbs_adjunction]
C
choice_Choice__to__eqtype_hasDecEq [definition, in QBS.qbs_quotient]choice_Choice__to__choice_hasChoice [definition, in QBS.qbs_quotient]
complete_the_square [lemma, in QBS.normal_algebra]
const_kernel_of_qbs_measurable [lemma, in QBS.qbs_kernel]
const_kernel_of_qbs [definition, in QBS.qbs_kernel]
coprodQ [definition, in QBS.coproduct_qbs]
coprodQ_Mx_glue [lemma, in QBS.coproduct_qbs]
coprodQ_Mx_const [lemma, in QBS.coproduct_qbs]
coprodQ_Mx_comp [lemma, in QBS.coproduct_qbs]
coprodQ_random [definition, in QBS.coproduct_qbs]
coproduct_qbs.listQ_instance.ax3 [variable, in QBS.coproduct_qbs]
coproduct_qbs.listQ_instance.ax2 [variable, in QBS.coproduct_qbs]
coproduct_qbs.listQ_instance.ax1 [variable, in QBS.coproduct_qbs]
coproduct_qbs.listQ_instance.Mx [variable, in QBS.coproduct_qbs]
coproduct_qbs.listQ_instance.x0 [variable, in QBS.coproduct_qbs]
coproduct_qbs.listQ_instance.X [variable, in QBS.coproduct_qbs]
coproduct_qbs.listQ_instance [section, in QBS.coproduct_qbs]
coproduct_qbs.piQ_instance.ax3 [variable, in QBS.coproduct_qbs]
coproduct_qbs.piQ_instance.ax2 [variable, in QBS.coproduct_qbs]
coproduct_qbs.piQ_instance.ax1 [variable, in QBS.coproduct_qbs]
coproduct_qbs.piQ_instance.Mx [variable, in QBS.coproduct_qbs]
coproduct_qbs.piQ_instance.X [variable, in QBS.coproduct_qbs]
coproduct_qbs.piQ_instance.I [variable, in QBS.coproduct_qbs]
coproduct_qbs.piQ_instance [section, in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance.ax3 [variable, in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance.ax2 [variable, in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance.ax1 [variable, in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance.Mx [variable, in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance.inh [variable, in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance.X [variable, in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance.I [variable, in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance.d [variable, in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance [section, in QBS.coproduct_qbs]
coproduct_qbs.coprodQ_instance.ax3 [variable, in QBS.coproduct_qbs]
coproduct_qbs.coprodQ_instance.ax2 [variable, in QBS.coproduct_qbs]
coproduct_qbs.coprodQ_instance.ax1 [variable, in QBS.coproduct_qbs]
coproduct_qbs.coprodQ_instance.Mx [variable, in QBS.coproduct_qbs]
coproduct_qbs.coprodQ_instance.Y [variable, in QBS.coproduct_qbs]
coproduct_qbs.coprodQ_instance.X [variable, in QBS.coproduct_qbs]
coproduct_qbs.coprodQ_instance [section, in QBS.coproduct_qbs]
coproduct_qbs.R [variable, in QBS.coproduct_qbs]
coproduct_qbs [section, in QBS.coproduct_qbs]
coproduct_qbs [library]
D
d [definition, in QBS.showcase.bayesian_regression]Datatypes_list__canonical__quasi_borel_QBSpace [definition, in QBS.coproduct_qbs]
Datatypes_sum__canonical__quasi_borel_QBSpace [definition, in QBS.coproduct_qbs]
Datatypes_unit__canonical__quasi_borel_QBSpace [definition, in QBS.quasi_borel]
Datatypes_prod__canonical__quasi_borel_QBSpace [definition, in QBS.quasi_borel]
decode_RR_mR [definition, in QBS.standard_borel]
decode_RRK [lemma, in QBS.standard_borel]
decode_RR [definition, in QBS.standard_borel]
deinterleave_interleaveK_odd [lemma, in QBS.standard_borel]
deinterleave_interleaveK_even [lemma, in QBS.standard_borel]
deinterleave_odd [definition, in QBS.standard_borel]
deinterleave_even [definition, in QBS.standard_borel]
d_le_peak [lemma, in QBS.showcase.bayesian_regression]
d_ge0 [lemma, in QBS.showcase.bayesian_regression]
E
encode_decode_kcomp_noparam [lemma, in QBS.qbs_kernel]encode_RR_mRK [lemma, in QBS.standard_borel]
encode_RR_mR [definition, in QBS.standard_borel]
encode_RRK [lemma, in QBS.standard_borel]
encode_RR [definition, in QBS.standard_borel]
erealQ [definition, in QBS.measure_qbs_adjunction]
ereal_standard_borel [lemma, in QBS.measure_qbs_adjunction]
evidence [definition, in QBS.showcase.bayesian_regression]
evidence_pos [lemma, in QBS.showcase.bayesian_regression]
evidence_value [lemma, in QBS.showcase.bayesian_regression]
evidence_eq [lemma, in QBS.showcase.bayesian_regression]
evidence_ge0 [lemma, in QBS.showcase.bayesian_regression]
expectation_prod_indep [lemma, in QBS.pair_qbs_measure]
expectation_prod_snd [lemma, in QBS.pair_qbs_measure]
expectation_prod_fst [lemma, in QBS.pair_qbs_measure]
expQ [definition, in QBS.quasi_borel]
expQ_Mx_glue [lemma, in QBS.quasi_borel]
expQ_Mx_const [lemma, in QBS.quasi_borel]
expQ_Mx_comp [lemma, in QBS.quasi_borel]
G
gaussian_prod_scalar_gt0 [lemma, in QBS.normal_algebra]gaussian_prod_sigma_neq0 [lemma, in QBS.normal_algebra]
gaussian_prod_sigma_sqr [lemma, in QBS.normal_algebra]
gaussian_prod_scalar [definition, in QBS.normal_algebra]
gaussian_prod_sigma [definition, in QBS.normal_algebra]
gaussian_prod_mu [definition, in QBS.normal_algebra]
generating_qbs_least [lemma, in QBS.quasi_borel]
generating_qbs_incl [lemma, in QBS.quasi_borel]
generating_qbs [definition, in QBS.quasi_borel]
generating_Mx_sind [definition, in QBS.quasi_borel]
generating_Mx_ind [definition, in QBS.quasi_borel]
generating_Mx [inductive, in QBS.quasi_borel]
generic_quotient_EqQuotient__to__generic_quotient_isEqQuotient [definition, in QBS.qbs_quotient]
generic_quotient_EqQuotient__to__generic_quotient_isQuotient [definition, in QBS.qbs_quotient]
gen_coprodQ [definition, in QBS.coproduct_qbs]
gen_coprodQ_Mx_glue [lemma, in QBS.coproduct_qbs]
gen_coprodQ_Mx_const [lemma, in QBS.coproduct_qbs]
gen_coprodQ_Mx_comp [lemma, in QBS.coproduct_qbs]
gen_coprodQ_random [definition, in QBS.coproduct_qbs]
gen_glue [constructor, in QBS.quasi_borel]
gen_const [constructor, in QBS.quasi_borel]
gen_comp [constructor, in QBS.quasi_borel]
gen_base [constructor, in QBS.quasi_borel]
geom_half_sum [lemma, in QBS.standard_borel]
giry_to_qbsK [lemma, in QBS.qbs_giry]
giry_to_qbs [definition, in QBS.qbs_giry]
H
half2 [lemma, in QBS.standard_borel]HB_unnamed_factory_7 [definition, in QBS.coproduct_qbs]
HB_unnamed_factory_5 [definition, in QBS.coproduct_qbs]
HB_unnamed_factory_3 [definition, in QBS.coproduct_qbs]
HB_unnamed_factory_1 [definition, in QBS.coproduct_qbs]
HB_unnamed_mixin_18 [definition, in QBS.probability_qbs]
HB_unnamed_mixin_17 [definition, in QBS.probability_qbs]
HB_unnamed_mixin_16 [definition, in QBS.probability_qbs]
HB_unnamed_mixin_15 [definition, in QBS.probability_qbs]
HB_unnamed_mixin_14 [definition, in QBS.probability_qbs]
HB_unnamed_factory_8 [definition, in QBS.probability_qbs]
HB_unnamed_mixin_7 [definition, in QBS.probability_qbs]
HB_unnamed_mixin_6 [definition, in QBS.probability_qbs]
HB_unnamed_factory_3 [definition, in QBS.probability_qbs]
HB_unnamed_factory_1 [definition, in QBS.probability_qbs]
HB_unnamed_factory_1 [definition, in QBS.qbs_prob_quot]
HB_unnamed_mixin_39 [definition, in QBS.qbs_giry]
HB_unnamed_mixin_38 [definition, in QBS.qbs_giry]
HB_unnamed_mixin_37 [definition, in QBS.qbs_giry]
HB_unnamed_mixin_36 [definition, in QBS.qbs_giry]
HB_unnamed_mixin_35 [definition, in QBS.qbs_giry]
HB_unnamed_factory_24 [definition, in QBS.qbs_giry]
HB_unnamed_mixin_23 [definition, in QBS.qbs_giry]
HB_unnamed_mixin_22 [definition, in QBS.qbs_giry]
HB_unnamed_factory_17 [definition, in QBS.qbs_giry]
HB_unnamed_mixin_16 [definition, in QBS.qbs_giry]
HB_unnamed_mixin_15 [definition, in QBS.qbs_giry]
HB_unnamed_mixin_14 [definition, in QBS.qbs_giry]
HB_unnamed_mixin_13 [definition, in QBS.qbs_giry]
HB_unnamed_mixin_12 [definition, in QBS.qbs_giry]
HB_unnamed_factory_6 [definition, in QBS.qbs_giry]
HB_unnamed_mixin_5 [definition, in QBS.qbs_giry]
HB_unnamed_mixin_4 [definition, in QBS.qbs_giry]
HB_unnamed_factory_1 [definition, in QBS.qbs_giry]
HB_unnamed_mixin_16 [definition, in QBS.pair_qbs_measure]
HB_unnamed_mixin_15 [definition, in QBS.pair_qbs_measure]
HB_unnamed_mixin_14 [definition, in QBS.pair_qbs_measure]
HB_unnamed_mixin_13 [definition, in QBS.pair_qbs_measure]
HB_unnamed_mixin_12 [definition, in QBS.pair_qbs_measure]
HB_unnamed_factory_6 [definition, in QBS.pair_qbs_measure]
HB_unnamed_mixin_5 [definition, in QBS.pair_qbs_measure]
HB_unnamed_mixin_4 [definition, in QBS.pair_qbs_measure]
HB_unnamed_factory_1 [definition, in QBS.pair_qbs_measure]
HB_unnamed_mixin_15 [definition, in QBS.qbs_quotient]
HB_unnamed_mixin_14 [definition, in QBS.qbs_quotient]
HB_unnamed_factory_10 [definition, in QBS.qbs_quotient]
HB_unnamed_mixin_9 [definition, in QBS.qbs_quotient]
HB_unnamed_mixin_8 [definition, in QBS.qbs_quotient]
HB_unnamed_factory_5 [definition, in QBS.qbs_quotient]
HB_unnamed_factory_3 [definition, in QBS.qbs_quotient]
HB_unnamed_factory_1 [definition, in QBS.qbs_quotient]
HB_unnamed_factory_34 [definition, in QBS.quasi_borel]
HB_unnamed_factory_32 [definition, in QBS.quasi_borel]
HB_unnamed_factory_29 [definition, in QBS.quasi_borel]
HB_unnamed_factory_27 [definition, in QBS.quasi_borel]
HB_unnamed_factory_25 [definition, in QBS.quasi_borel]
HB_unnamed_factory_22 [definition, in QBS.quasi_borel]
HB_unnamed_factory_20 [definition, in QBS.quasi_borel]
HB_unnamed_factory_18 [definition, in QBS.quasi_borel]
HB_unnamed_factory_15 [definition, in QBS.quasi_borel]
HB_unnamed_factory_12 [definition, in QBS.quasi_borel]
HB_unnamed_factory_10 [definition, in QBS.quasi_borel]
HB_unnamed_factory_8 [definition, in QBS.quasi_borel]
HB_unnamed_factory_5 [definition, in QBS.quasi_borel]
HB_unnamed_factory_3 [definition, in QBS.quasi_borel]
HB_unnamed_factory_1 [definition, in QBS.quasi_borel]
I
integral_normal_prob [lemma, in QBS.showcase.bayesian_regression]integral_normal_prob.R [variable, in QBS.showcase.bayesian_regression]
integral_normal_prob [section, in QBS.showcase.bayesian_regression]
integral_normal_prob [lemma, in QBS.measure_as_qbs_measure]
intercept_prior [definition, in QBS.showcase.bayesian_regression]
interleave [definition, in QBS.standard_borel]
interleave_no_trailing_ones [lemma, in QBS.standard_borel]
interleave_deinterleaveK [lemma, in QBS.standard_borel]
inv_cvg_approx [lemma, in QBS.standard_borel]
isQBS [abbreviation, in QBS.quasi_borel]
isQBS [module, in QBS.quasi_borel]
isQBSMorphism [abbreviation, in QBS.quasi_borel]
isQBSMorphism [module, in QBS.quasi_borel]
isQBSMorphism.axioms [abbreviation, in QBS.quasi_borel]
isQBSMorphism.axioms_ [record, in QBS.quasi_borel]
isQBSMorphism.Build [abbreviation, in QBS.quasi_borel]
isQBSMorphism.Exports [module, in QBS.quasi_borel]
isQBSMorphism.identity_builder [definition, in QBS.quasi_borel]
isQBSMorphism.isQBSMorphism.f [variable, in QBS.quasi_borel]
isQBSMorphism.isQBSMorphism.isQBSMorphism [section, in QBS.quasi_borel]
isQBSMorphism.isQBSMorphism.R [variable, in QBS.quasi_borel]
isQBSMorphism.isQBSMorphism.X [variable, in QBS.quasi_borel]
isQBSMorphism.isQBSMorphism.Y [variable, in QBS.quasi_borel]
isQBSMorphism.phant_axioms [definition, in QBS.quasi_borel]
isQBSMorphism.phant_Build [definition, in QBS.quasi_borel]
isQBSMorphism.qbs_hom_proof [projection, in QBS.quasi_borel]
isQBS.axioms [abbreviation, in QBS.quasi_borel]
isQBS.axioms_ [record, in QBS.quasi_borel]
isQBS.Build [abbreviation, in QBS.quasi_borel]
isQBS.Exports [module, in QBS.quasi_borel]
isQBS.identity_builder [definition, in QBS.quasi_borel]
isQBS.isQBS.isQBS [section, in QBS.quasi_borel]
isQBS.isQBS.R [variable, in QBS.quasi_borel]
isQBS.isQBS.T [variable, in QBS.quasi_borel]
isQBS.phant_axioms [definition, in QBS.quasi_borel]
isQBS.phant_Build [definition, in QBS.quasi_borel]
isQBS.qbs_Mx_glue [projection, in QBS.quasi_borel]
isQBS.qbs_Mx_const [projection, in QBS.quasi_borel]
isQBS.qbs_Mx_comp [projection, in QBS.quasi_borel]
isQBS.qbs_Mx [projection, in QBS.quasi_borel]
is_cvg_bin_partial_sum [lemma, in QBS.standard_borel]
K
kdiracE [lemma, in QBS.qbs_kernel]kdirac_round_trip [lemma, in QBS.qbs_kernel]
kdirac_comp_noparam [lemma, in QBS.qbs_kernel]
kdirac_comp [lemma, in QBS.qbs_kernel]
kdirac_measurable_kernel [lemma, in QBS.qbs_kernel]
kernel_round_trip [lemma, in QBS.qbs_kernel]
kernel_integration [lemma, in QBS.qbs_kernel]
L
likelihood_single_strong [lemma, in QBS.showcase.bayesian_regression]likelihood_single_morphism [lemma, in QBS.showcase.bayesian_regression]
likelihood_single [definition, in QBS.showcase.bayesian_regression]
listQ [definition, in QBS.coproduct_qbs]
listQ_nth_random [lemma, in QBS.coproduct_qbs]
listQ_Mx_glue [lemma, in QBS.coproduct_qbs]
listQ_Mx_const [lemma, in QBS.coproduct_qbs]
listQ_Mx_comp [lemma, in QBS.coproduct_qbs]
listQ_random [definition, in QBS.coproduct_qbs]
lr_adj_iff [lemma, in QBS.measure_qbs_adjunction]
lr_adj_r2l [lemma, in QBS.measure_qbs_adjunction]
lr_adj_l2r [lemma, in QBS.measure_qbs_adjunction]
L_qbs_comp [lemma, in QBS.measure_qbs_adjunction]
L_qbs_id [lemma, in QBS.measure_qbs_adjunction]
L_qbs_morph [lemma, in QBS.measure_qbs_adjunction]
L_sigma_bigcup [lemma, in QBS.measure_qbs_adjunction]
L_sigma_setC [lemma, in QBS.measure_qbs_adjunction]
L_sigma_setT [lemma, in QBS.measure_qbs_adjunction]
L_sigma [abbreviation, in QBS.measure_qbs_adjunction]
L_sigma_set0 [lemma, in QBS.measure_qbs_adjunction]
M
map_qbs_morph_from [lemma, in QBS.quasi_borel]map_qbs_morphism_out [lemma, in QBS.quasi_borel]
map_qbs_sub [lemma, in QBS.quasi_borel]
map_qbs_random [lemma, in QBS.quasi_borel]
map_qbs [definition, in QBS.quasi_borel]
measfun_kernel_prob [lemma, in QBS.qbs_kernel]
measfun_kernel [definition, in QBS.qbs_kernel]
measurable_contract [lemma, in QBS.measure_qbs_adjunction]
measurable_contract_fin [lemma, in QBS.measure_qbs_adjunction]
measurable_truncn [lemma, in QBS.measure_qbs_adjunction]
measurable_fun_nat_discrete [lemma, in QBS.measure_qbs_adjunction]
Measurable_sort__canonical__quasi_borel_QBSpace [definition, in QBS.quasi_borel]
measurable_glue [lemma, in QBS.quasi_borel]
measurable_R_to_RR [lemma, in QBS.standard_borel]
measurable_RR_to_R [lemma, in QBS.standard_borel]
measurable_decode_RR [lemma, in QBS.standard_borel]
measurable_psi_setT [lemma, in QBS.standard_borel]
measurable_encode_RR [lemma, in QBS.standard_borel]
measurable_unit_to_pair_snd [lemma, in QBS.standard_borel]
measurable_unit_to_pair_fst [lemma, in QBS.standard_borel]
measurable_pair_to_unit [lemma, in QBS.standard_borel]
measurable_bool_scale [lemma, in QBS.standard_borel]
measurable_deinterleave_odd_digit [lemma, in QBS.standard_borel]
measurable_deinterleave_even_digit [lemma, in QBS.standard_borel]
measurable_interleave_digit [lemma, in QBS.standard_borel]
measurable_bin_digit [lemma, in QBS.standard_borel]
measurable_iter_step [lemma, in QBS.standard_borel]
measurable_step [lemma, in QBS.standard_borel]
measurable_psi [lemma, in QBS.standard_borel]
measurable_phi [lemma, in QBS.standard_borel]
measure_function_isMeasure__to__measure_function_isContent [definition, in QBS.probability_qbs]
measure_function_isMeasure__to__measure_function_Content_isMeasure [definition, in QBS.probability_qbs]
measure_function_isMeasure__to__measure_function_isContent__21 [definition, in QBS.qbs_giry]
measure_function_isMeasure__to__measure_function_Content_isMeasure__19 [definition, in QBS.qbs_giry]
measure_function_isMeasure__to__measure_function_isContent [definition, in QBS.qbs_giry]
measure_function_isMeasure__to__measure_function_Content_isMeasure [definition, in QBS.qbs_giry]
measure_function_isMeasure__to__measure_function_isContent [definition, in QBS.pair_qbs_measure]
measure_function_isMeasure__to__measure_function_Content_isMeasure [definition, in QBS.pair_qbs_measure]
measure_as_qbs.distribution_expectations [section, in QBS.measure_as_qbs_measure]
measure_as_qbs.R [variable, in QBS.measure_as_qbs_measure]
measure_as_qbs [section, in QBS.measure_as_qbs_measure]
measure_qbs_adjunction [library]
measure_as_qbs_measure [library]
monadP [definition, in QBS.probability_qbs]
monadP_map_comp [lemma, in QBS.probability_qbs]
monadP_map_id [lemma, in QBS.probability_qbs]
monadP_map_morph [lemma, in QBS.probability_qbs]
monadP_map [definition, in QBS.probability_qbs]
monadP_glue [lemma, in QBS.probability_qbs]
monadP_const [lemma, in QBS.probability_qbs]
monadP_comp [lemma, in QBS.probability_qbs]
monadP_random_impl [lemma, in QBS.probability_qbs]
monadP_random_pw [definition, in QBS.probability_qbs]
monadP_random [definition, in QBS.probability_qbs]
mqa [section, in QBS.measure_qbs_adjunction]
mqa.R [variable, in QBS.measure_qbs_adjunction]
mR [abbreviation, in QBS.coproduct_qbs]
mR [abbreviation, in QBS.qbs_kernel]
mR [abbreviation, in QBS.probability_qbs]
mR [abbreviation, in QBS.measure_qbs_adjunction]
mR [abbreviation, in QBS.qbs_prob_quot]
mR [abbreviation, in QBS.qbs_giry]
mR [abbreviation, in QBS.showcase.bayesian_regression]
mR [abbreviation, in QBS.pair_qbs_measure]
mR [abbreviation, in QBS.qbs_quotient]
mR [abbreviation, in QBS.measure_as_qbs_measure]
mR [abbreviation, in QBS.quasi_borel]
mR [abbreviation, in QBS.standard_borel]
mu [abbreviation, in QBS.showcase.bayesian_regression]
N
natQ [definition, in QBS.quasi_borel]nat_standard_borel [lemma, in QBS.measure_qbs_adjunction]
nine_div_gt0 [lemma, in QBS.normal_algebra]
noise_sigma_neq0 [lemma, in QBS.showcase.bayesian_regression]
normalize_prob [definition, in QBS.probability_qbs]
normalize_alpha_random [lemma, in QBS.probability_qbs]
normalize_mu [definition, in QBS.probability_qbs]
normal_pdf_recenter [lemma, in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.mu3_s [variable, in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.mu2_s [variable, in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.mu1_s [variable, in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.mu0_s [variable, in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.sigma3 [variable, in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.W45 [variable, in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.sigma2 [variable, in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.W34 [variable, in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.sigma1 [variable, in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.W23 [variable, in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.sigma0 [variable, in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.W12 [variable, in QBS.normal_algebra]
normal_fun_linear [lemma, in QBS.normal_algebra]
normal_fun_sub [lemma, in QBS.normal_algebra]
normal_fun_sym [lemma, in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope [section, in QBS.normal_algebra]
normal_density_algebra.bayesian_phase1_intercept [section, in QBS.normal_algebra]
normal_pdf_times_chain [lemma, in QBS.normal_algebra]
normal_pdf_times' [lemma, in QBS.normal_algebra]
normal_pdf_times [lemma, in QBS.normal_algebra]
normal_density_algebra.normal_pdf_general [section, in QBS.normal_algebra]
normal_density_algebra.three_neq0 [variable, in QBS.normal_algebra]
normal_density_algebra.half_neq0 [variable, in QBS.normal_algebra]
normal_density_algebra.R [variable, in QBS.normal_algebra]
normal_density_algebra [section, in QBS.normal_algebra]
normal_algebra [library]
norm_qbs_none [lemma, in QBS.showcase.bayesian_regression]
norm_qbs_some [lemma, in QBS.showcase.bayesian_regression]
norm_qbs [definition, in QBS.showcase.bayesian_regression]
no_trailing_ones_shift [lemma, in QBS.standard_borel]
no_trailing_ones [definition, in QBS.standard_borel]
O
obs [definition, in QBS.showcase.bayesian_regression]obs_product_integrable [lemma, in QBS.showcase.bayesian_regression]
obs_int_proof [lemma, in QBS.showcase.bayesian_regression]
obs_meas_proof [lemma, in QBS.showcase.bayesian_regression]
obs_ub [lemma, in QBS.showcase.bayesian_regression]
obs_ge0 [lemma, in QBS.showcase.bayesian_regression]
obs_rewrite [lemma, in QBS.normal_algebra]
P
pair_qbs_measure_pf_mu__canonical__probability_measure_Probability [definition, in QBS.pair_qbs_measure]pair_qbs_measure_pf_mu__canonical__probability_measure_SubProbability [definition, in QBS.pair_qbs_measure]
pair_qbs_measure_pf_mu__canonical__measure_function_FiniteMeasure [definition, in QBS.pair_qbs_measure]
pair_qbs_measure_pf_mu__canonical__measure_function_FinNumFun [definition, in QBS.pair_qbs_measure]
pair_qbs_measure_pf_mu__canonical__measure_function_SigmaFiniteMeasure [definition, in QBS.pair_qbs_measure]
pair_qbs_measure_pf_mu__canonical__measure_function_SFiniteMeasure [definition, in QBS.pair_qbs_measure]
pair_qbs_measure_pf_mu__canonical__measure_function_SigmaFiniteContent [definition, in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.pf_mu_setT [variable, in QBS.pair_qbs_measure]
pair_qbs_measure_pf_mu__canonical__measure_function_Measure [definition, in QBS.pair_qbs_measure]
pair_qbs_measure_pf_mu__canonical__measure_function_Content [definition, in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.pf_mu_sigma [variable, in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.pf_mu_ge0 [variable, in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.pf_mu0 [variable, in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.pf_mu [variable, in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.mu_q [variable, in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.mu_p [variable, in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.q [variable, in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.p [variable, in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.Y [variable, in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.X [variable, in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build [section, in QBS.pair_qbs_measure]
pair_qbs_measure.R [variable, in QBS.pair_qbs_measure]
pair_qbs_measure [section, in QBS.pair_qbs_measure]
pair_standard_borel [lemma, in QBS.standard_borel]
pair_to_unit_phi_in_01 [lemma, in QBS.standard_borel]
pair_to_unit_phi_in_itv [lemma, in QBS.standard_borel]
pair_to_unit_phi_lt1 [lemma, in QBS.standard_borel]
pair_to_unit_phi_gt0 [lemma, in QBS.standard_borel]
pair_to_unitK [lemma, in QBS.standard_borel]
pair_to_unit [definition, in QBS.standard_borel]
pair_qbs_measure [library]
phase1_integration [lemma, in QBS.showcase.bayesian_regression]
phase1_combine5 [lemma, in QBS.normal_algebra]
phase1_combine3 [lemma, in QBS.normal_algebra]
phase1_sqrtr_var5_neq0 [lemma, in QBS.normal_algebra]
phase1_sqrtr_var4_neq0 [lemma, in QBS.normal_algebra]
phase1_sqrtr_var3_neq0 [lemma, in QBS.normal_algebra]
phase1_sqrtr_var2_neq0 [lemma, in QBS.normal_algebra]
phase1_sqrtr_var1_neq0 [lemma, in QBS.normal_algebra]
phase1_step45_mu [lemma, in QBS.normal_algebra]
phase1_step45_sigma2 [lemma, in QBS.normal_algebra]
phase1_step34_mu [lemma, in QBS.normal_algebra]
phase1_step34_sigma2 [lemma, in QBS.normal_algebra]
phase1_step23_mu [lemma, in QBS.normal_algebra]
phase1_step23_sigma2 [lemma, in QBS.normal_algebra]
phase1_step12_mu [lemma, in QBS.normal_algebra]
phase1_step12_sigma2 [lemma, in QBS.normal_algebra]
phase1_step01_mu [lemma, in QBS.normal_algebra]
phase1_step01_sigma2 [lemma, in QBS.normal_algebra]
phase2_integration [lemma, in QBS.showcase.bayesian_regression]
phase2_combine5 [lemma, in QBS.normal_algebra]
phase2_const_gt0 [lemma, in QBS.normal_algebra]
phase2_final_sigma_neq0 [lemma, in QBS.normal_algebra]
phase2_const [definition, in QBS.normal_algebra]
phase2_final_sigma [definition, in QBS.normal_algebra]
phase2_final_mu [definition, in QBS.normal_algebra]
phase2_step4_sigma_neq0 [lemma, in QBS.normal_algebra]
phase2_step4 [lemma, in QBS.normal_algebra]
phase2_scalar45E [lemma, in QBS.normal_algebra]
phase2_W45_neq0 [lemma, in QBS.normal_algebra]
phase2_scalar45_fun [lemma, in QBS.normal_algebra]
phase2_S45 [lemma, in QBS.normal_algebra]
phase2_step3_sigma_neq0 [lemma, in QBS.normal_algebra]
phase2_step3 [lemma, in QBS.normal_algebra]
phase2_scalar34E [lemma, in QBS.normal_algebra]
phase2_W34_neq0 [lemma, in QBS.normal_algebra]
phase2_scalar34_fun [lemma, in QBS.normal_algebra]
phase2_S34 [lemma, in QBS.normal_algebra]
phase2_step2_sigma_neq0 [lemma, in QBS.normal_algebra]
phase2_step2 [lemma, in QBS.normal_algebra]
phase2_scalar23E [lemma, in QBS.normal_algebra]
phase2_W23_neq0 [lemma, in QBS.normal_algebra]
phase2_scalar23_fun [lemma, in QBS.normal_algebra]
phase2_S23 [lemma, in QBS.normal_algebra]
phase2_step1_sigma_neq0 [lemma, in QBS.normal_algebra]
phase2_step1_sigma2 [lemma, in QBS.normal_algebra]
phase2_step1 [lemma, in QBS.normal_algebra]
phase2_scalar12E [lemma, in QBS.normal_algebra]
phase2_W12_neq0 [lemma, in QBS.normal_algebra]
phase2_scalar12_fun [lemma, in QBS.normal_algebra]
phase2_S12 [lemma, in QBS.normal_algebra]
phase2_step0_sigma_neq0 [lemma, in QBS.normal_algebra]
phase2_step0_sigma2 [lemma, in QBS.normal_algebra]
phase2_step0 [lemma, in QBS.normal_algebra]
phase2_scalar01E [lemma, in QBS.normal_algebra]
phase2_scalar45_diff [lemma, in QBS.normal_algebra]
phase2_scalar34_diff [lemma, in QBS.normal_algebra]
phase2_scalar23_diff [lemma, in QBS.normal_algebra]
phase2_scalar12_diff [lemma, in QBS.normal_algebra]
phase2_scalar01_fun [lemma, in QBS.normal_algebra]
phase2_scalar01_diff [lemma, in QBS.normal_algebra]
phi [definition, in QBS.standard_borel]
phiK [lemma, in QBS.standard_borel]
phi_has_true_digit [lemma, in QBS.standard_borel]
phi_in_01 [lemma, in QBS.standard_borel]
phi_ge0 [lemma, in QBS.standard_borel]
phi_lt1 [lemma, in QBS.standard_borel]
phi_gt0 [lemma, in QBS.standard_borel]
phi_psi.R [variable, in QBS.standard_borel]
phi_psi [section, in QBS.standard_borel]
piQ [definition, in QBS.coproduct_qbs]
piQ_Mx_glue [lemma, in QBS.coproduct_qbs]
piQ_Mx_const [lemma, in QBS.coproduct_qbs]
piQ_Mx_comp [lemma, in QBS.coproduct_qbs]
piQ_random [definition, in QBS.coproduct_qbs]
piX [abbreviation, in QBS.qbs_quotient]
piX [abbreviation, in QBS.qbs_quotient]
piX [abbreviation, in QBS.qbs_quotient]
piY [abbreviation, in QBS.qbs_quotient]
piY [abbreviation, in QBS.qbs_quotient]
piY [abbreviation, in QBS.qbs_quotient]
posterior_measure_characterization [lemma, in QBS.showcase.bayesian_regression]
posterior_density_eq [lemma, in QBS.showcase.bayesian_regression]
posterior_density_total [lemma, in QBS.showcase.bayesian_regression]
posterior_density [definition, in QBS.showcase.bayesian_regression]
predictive_marginal [lemma, in QBS.showcase.bayesian_regression]
predictive_integral [definition, in QBS.showcase.bayesian_regression]
prior [definition, in QBS.showcase.bayesian_regression]
prior_bind [definition, in QBS.showcase.bayesian_regression]
prior_bind_diag [lemma, in QBS.showcase.bayesian_regression]
prior_inner [definition, in QBS.showcase.bayesian_regression]
prior_inner_diag [lemma, in QBS.showcase.bayesian_regression]
prior_sigma_gt0 [lemma, in QBS.showcase.bayesian_regression]
probability_fin_num_fun [lemma, in QBS.qbs_kernel]
probability_qbs.qbs_normalize_def.X [variable, in QBS.probability_qbs]
probability_qbs.qbs_normalize_def [section, in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__probability_measure_Probability [definition, in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__probability_measure_SubProbability [definition, in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__measure_function_FiniteMeasure [definition, in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__measure_function_FinNumFun [definition, in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__measure_function_SigmaFiniteMeasure [definition, in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__measure_function_SFiniteMeasure [definition, in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__measure_function_SigmaFiniteContent [definition, in QBS.probability_qbs]
probability_measure_Measure_isProbability__to__measure_function_isFinite [definition, in QBS.probability_qbs]
probability_measure_Measure_isProbability__to__measure_function_isSFinite [definition, in QBS.probability_qbs]
probability_measure_Measure_isProbability__to__probability_measure_isSubProbability [definition, in QBS.probability_qbs]
probability_measure_Measure_isProbability__to__measure_function_isSigmaFinite [definition, in QBS.probability_qbs]
probability_measure_Measure_isProbability__to__probability_measure_isProbability [definition, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.norm_mu_setT [variable, in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__measure_function_Measure [definition, in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__measure_function_Content [definition, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.norm_mu_sigma [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.norm_mu_ge0 [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.norm_mu0 [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.norm_mu [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.wdiv_meas [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.wdiv_ge0 [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.wdiv [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.ev_r_neq0 [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.ev_r_gt0 [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.ev_r [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.hev_fin [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.hev_pos [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.ev [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.hw_meas [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.hw_ge0 [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.w [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.p [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build.X [variable, in QBS.probability_qbs]
probability_qbs.normalize_mu_build [section, in QBS.probability_qbs]
probability_qbs.probability_inequalities [section, in QBS.probability_qbs]
probability_qbs.strength_and_monad_structure [section, in QBS.probability_qbs]
probability_qbs.bind_congruence [section, in QBS.probability_qbs]
probability_qbs.monad_operations [section, in QBS.probability_qbs]
probability_qbs.qbs_integration [section, in QBS.probability_qbs]
probability_qbs.monad_bind [section, in QBS.probability_qbs]
probability_qbs_qbs_prob__canonical__quasi_borel_QBSpace [definition, in QBS.probability_qbs]
probability_qbs.probability_monad.monadP_instance.ax_glue [variable, in QBS.probability_qbs]
probability_qbs.probability_monad.monadP_instance.ax_const [variable, in QBS.probability_qbs]
probability_qbs.probability_monad.monadP_instance.ax_comp [variable, in QBS.probability_qbs]
probability_qbs.probability_monad.monadP_instance.Mx [variable, in QBS.probability_qbs]
probability_qbs.probability_monad.monadP_instance.X [variable, in QBS.probability_qbs]
probability_qbs.probability_monad.monadP_instance [section, in QBS.probability_qbs]
probability_qbs.probability_monad [section, in QBS.probability_qbs]
probability_qbs.qbs_prob_basics [section, in QBS.probability_qbs]
probability_qbs.R [variable, in QBS.probability_qbs]
probability_qbs [section, in QBS.probability_qbs]
probability_measure_Measure_isProbability__to__measure_function_isFinite__34 [definition, in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__measure_function_isSFinite__32 [definition, in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__probability_measure_isSubProbability__30 [definition, in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__measure_function_isSigmaFinite__28 [definition, in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__probability_measure_isProbability__26 [definition, in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__measure_function_isFinite [definition, in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__measure_function_isSFinite [definition, in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__probability_measure_isSubProbability [definition, in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__measure_function_isSigmaFinite [definition, in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__probability_measure_isProbability [definition, in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__measure_function_isFinite [definition, in QBS.pair_qbs_measure]
probability_measure_Measure_isProbability__to__measure_function_isSFinite [definition, in QBS.pair_qbs_measure]
probability_measure_Measure_isProbability__to__probability_measure_isSubProbability [definition, in QBS.pair_qbs_measure]
probability_measure_Measure_isProbability__to__measure_function_isSigmaFinite [definition, in QBS.pair_qbs_measure]
probability_measure_Measure_isProbability__to__probability_measure_isProbability [definition, in QBS.pair_qbs_measure]
probability_qbs_qbs_prob__canonical__choice_Choice [definition, in QBS.qbs_quotient]
probability_qbs_qbs_prob__canonical__eqtype_Equality [definition, in QBS.qbs_quotient]
probability_qbs [library]
prob_sfinite_measure [lemma, in QBS.qbs_kernel]
prodQ [definition, in QBS.quasi_borel]
prodQ_random_const [lemma, in QBS.quasi_borel]
prodQ_const_random [lemma, in QBS.quasi_borel]
prodQ_Mx_glue [lemma, in QBS.quasi_borel]
prodQ_Mx_const [lemma, in QBS.quasi_borel]
prodQ_Mx_comp [lemma, in QBS.quasi_borel]
prod__canonical__quasi_borel_QBSpace [definition, in QBS.coproduct_qbs]
prod_standard_borel [lemma, in QBS.measure_qbs_adjunction]
program [definition, in QBS.showcase.bayesian_regression]
program_integrates_to_1 [lemma, in QBS.showcase.bayesian_regression]
program_succeeds [lemma, in QBS.showcase.bayesian_regression]
psi [definition, in QBS.standard_borel]
psiK [lemma, in QBS.standard_borel]
pushforward_probability [lemma, in QBS.qbs_kernel]
Q
qbs [section, in QBS.quasi_borel]QBSHom [abbreviation, in QBS.quasi_borel]
QBSHom [module, in QBS.quasi_borel]
QBSHomElpiOperations [module, in QBS.quasi_borel]
QBSHom_type__canonical__quasi_borel_QBSpace [definition, in QBS.quasi_borel]
QBSHom.axioms_ [record, in QBS.quasi_borel]
QBSHom.class [projection, in QBS.quasi_borel]
QBSHom.clone [abbreviation, in QBS.quasi_borel]
QBSHom.copy [abbreviation, in QBS.quasi_borel]
QBSHom.Exports [module, in QBS.quasi_borel]
QBSHom.Exports.qbsHomType [abbreviation, in QBS.quasi_borel]
QBSHom.on [abbreviation, in QBS.quasi_borel]
QBSHom.on_ [abbreviation, in QBS.quasi_borel]
QBSHom.pack_ [definition, in QBS.quasi_borel]
QBSHom.phant_on_ [definition, in QBS.quasi_borel]
QBSHom.phant_clone [definition, in QBS.quasi_borel]
QBSHom.quasi_borel_isQBSMorphism_mixin [projection, in QBS.quasi_borel]
QBSHom.sort [projection, in QBS.quasi_borel]
QBSHom.type [record, in QBS.quasi_borel]
QBSpace [abbreviation, in QBS.quasi_borel]
QBSpace [module, in QBS.quasi_borel]
QBSpaceElpiOperations [module, in QBS.quasi_borel]
QBSpace.axioms_ [record, in QBS.quasi_borel]
QBSpace.class [projection, in QBS.quasi_borel]
QBSpace.clone [abbreviation, in QBS.quasi_borel]
QBSpace.copy [abbreviation, in QBS.quasi_borel]
QBSpace.Exports [module, in QBS.quasi_borel]
QBSpace.Exports.qbsType [abbreviation, in QBS.quasi_borel]
QBSpace.on [abbreviation, in QBS.quasi_borel]
QBSpace.on_ [abbreviation, in QBS.quasi_borel]
QBSpace.pack_ [definition, in QBS.quasi_borel]
QBSpace.phant_on_ [definition, in QBS.quasi_borel]
QBSpace.phant_clone [definition, in QBS.quasi_borel]
QBSpace.quasi_borel_isQBS_mixin [projection, in QBS.quasi_borel]
QBSpace.sort [projection, in QBS.quasi_borel]
QBSpace.type [record, in QBS.quasi_borel]
qbs_morphism_length [lemma, in QBS.coproduct_qbs]
qbs_morphism_gen_to_coprod [lemma, in QBS.coproduct_qbs]
qbs_morphism_coprod_to_gen [lemma, in QBS.coproduct_qbs]
qbs_morphism_tuple [lemma, in QBS.coproduct_qbs]
qbs_morphism_proj [lemma, in QBS.coproduct_qbs]
qbs_morphism_gen_inj [lemma, in QBS.coproduct_qbs]
qbs_coprod_eta [lemma, in QBS.coproduct_qbs]
qbs_morphism_case_inr [lemma, in QBS.coproduct_qbs]
qbs_morphism_case_inl [lemma, in QBS.coproduct_qbs]
qbs_morphism_case [lemma, in QBS.coproduct_qbs]
qbs_morphism_inr [lemma, in QBS.coproduct_qbs]
qbs_morphism_inl [lemma, in QBS.coproduct_qbs]
qbs_kernel.round_trip.decode_encode [variable, in QBS.qbs_kernel]
qbs_kernel.round_trip.decode_meas [variable, in QBS.qbs_kernel]
qbs_kernel.round_trip.encode_meas [variable, in QBS.qbs_kernel]
qbs_kernel.round_trip.decode [variable, in QBS.qbs_kernel]
qbs_kernel.round_trip.encode [variable, in QBS.qbs_kernel]
qbs_kernel.round_trip.M [variable, in QBS.qbs_kernel]
qbs_kernel.round_trip.d [variable, in QBS.qbs_kernel]
qbs_kernel.round_trip [section, in QBS.qbs_kernel]
qbs_kernel.integration.M [variable, in QBS.qbs_kernel]
qbs_kernel.integration.d [variable, in QBS.qbs_kernel]
qbs_kernel.integration [section, in QBS.qbs_kernel]
qbs_bind_return_map [lemma, in QBS.qbs_kernel]
qbs_kernel.bind_return.M2 [variable, in QBS.qbs_kernel]
qbs_kernel.bind_return.M1 [variable, in QBS.qbs_kernel]
qbs_kernel.bind_return.d2 [variable, in QBS.qbs_kernel]
qbs_kernel.bind_return.d1 [variable, in QBS.qbs_kernel]
qbs_kernel.bind_return [section, in QBS.qbs_kernel]
qbs_kernel.dirac_comp.M2 [variable, in QBS.qbs_kernel]
qbs_kernel.dirac_comp.M1 [variable, in QBS.qbs_kernel]
qbs_kernel.dirac_comp.d2 [variable, in QBS.qbs_kernel]
qbs_kernel.dirac_comp.d1 [variable, in QBS.qbs_kernel]
qbs_kernel.dirac_comp [section, in QBS.qbs_kernel]
qbs_giry_pushforward [lemma, in QBS.qbs_kernel]
qbs_to_giry_map [lemma, in QBS.qbs_kernel]
qbs_kernel.giry_pushforward.M2 [variable, in QBS.qbs_kernel]
qbs_kernel.giry_pushforward.M1 [variable, in QBS.qbs_kernel]
qbs_kernel.giry_pushforward.d2 [variable, in QBS.qbs_kernel]
qbs_kernel.giry_pushforward.d1 [variable, in QBS.qbs_kernel]
qbs_kernel.giry_pushforward [section, in QBS.qbs_kernel]
qbs_prob_equiv_giry [lemma, in QBS.qbs_kernel]
qbs_kernel.equiv_kernel.M [variable, in QBS.qbs_kernel]
qbs_kernel.equiv_kernel.d [variable, in QBS.qbs_kernel]
qbs_kernel.equiv_kernel [section, in QBS.qbs_kernel]
qbs_kernel.const_kernel.M [variable, in QBS.qbs_kernel]
qbs_kernel.const_kernel.d [variable, in QBS.qbs_kernel]
qbs_kernel.const_kernel [section, in QBS.qbs_kernel]
qbs_kernel.kdirac_measurability.M2 [variable, in QBS.qbs_kernel]
qbs_kernel.kdirac_measurability.M1 [variable, in QBS.qbs_kernel]
qbs_kernel.kdirac_measurability.d2 [variable, in QBS.qbs_kernel]
qbs_kernel.kdirac_measurability.d1 [variable, in QBS.qbs_kernel]
qbs_kernel.kdirac_measurability [section, in QBS.qbs_kernel]
qbs_morph_kdirac_prob [lemma, in QBS.qbs_kernel]
qbs_morph_kdirac [definition, in QBS.qbs_kernel]
qbs_morph_measurable [lemma, in QBS.qbs_kernel]
qbs_kernel.qbs_morph_kernel.sb2 [variable, in QBS.qbs_kernel]
qbs_kernel.qbs_morph_kernel.sb1 [variable, in QBS.qbs_kernel]
qbs_kernel.qbs_morph_kernel.M2 [variable, in QBS.qbs_kernel]
qbs_kernel.qbs_morph_kernel.M1 [variable, in QBS.qbs_kernel]
qbs_kernel.qbs_morph_kernel.d2 [variable, in QBS.qbs_kernel]
qbs_kernel.qbs_morph_kernel.d1 [variable, in QBS.qbs_kernel]
qbs_kernel.qbs_morph_kernel [section, in QBS.qbs_kernel]
qbs_return_to_dirac [lemma, in QBS.qbs_kernel]
qbs_kernel.qbs_return_dirac.decode_encode [variable, in QBS.qbs_kernel]
qbs_kernel.qbs_return_dirac.decode_meas [variable, in QBS.qbs_kernel]
qbs_kernel.qbs_return_dirac.encode_meas [variable, in QBS.qbs_kernel]
qbs_kernel.qbs_return_dirac.decode [variable, in QBS.qbs_kernel]
qbs_kernel.qbs_return_dirac.encode [variable, in QBS.qbs_kernel]
qbs_kernel.qbs_return_dirac.M [variable, in QBS.qbs_kernel]
qbs_kernel.qbs_return_dirac.d [variable, in QBS.qbs_kernel]
qbs_kernel.qbs_return_dirac [section, in QBS.qbs_kernel]
qbs_kernel.kdirac_unfold.M2 [variable, in QBS.qbs_kernel]
qbs_kernel.kdirac_unfold.M1 [variable, in QBS.qbs_kernel]
qbs_kernel.kdirac_unfold.d2 [variable, in QBS.qbs_kernel]
qbs_kernel.kdirac_unfold.d1 [variable, in QBS.qbs_kernel]
qbs_kernel.kdirac_unfold [section, in QBS.qbs_kernel]
qbs_kernel.pushforward_prob.M2 [variable, in QBS.qbs_kernel]
qbs_kernel.pushforward_prob.M1 [variable, in QBS.qbs_kernel]
qbs_kernel.pushforward_prob.d2 [variable, in QBS.qbs_kernel]
qbs_kernel.pushforward_prob.d1 [variable, in QBS.qbs_kernel]
qbs_kernel.pushforward_prob [section, in QBS.qbs_kernel]
qbs_prob_sfinite [lemma, in QBS.qbs_kernel]
qbs_kernel.R [variable, in QBS.qbs_kernel]
qbs_kernel [section, in QBS.qbs_kernel]
qbs_normalize_integral [lemma, in QBS.probability_qbs]
qbs_normalize_total [lemma, in QBS.probability_qbs]
qbs_normalize_alpha [lemma, in QBS.probability_qbs]
qbs_normalize [definition, in QBS.probability_qbs]
qbs_strength_law4 [lemma, in QBS.probability_qbs]
qbs_strength_law4_diag [lemma, in QBS.probability_qbs]
qbs_chebyshev [lemma, in QBS.probability_qbs]
qbs_markov [lemma, in QBS.probability_qbs]
qbs_rv [definition, in QBS.probability_qbs]
qbs_varianceZ [lemma, in QBS.probability_qbs]
qbs_varianceE [lemma, in QBS.probability_qbs]
qbs_integralZl [lemma, in QBS.probability_qbs]
qbs_integralB [lemma, in QBS.probability_qbs]
qbs_integralD [lemma, in QBS.probability_qbs]
qbs_integrableZl [lemma, in QBS.probability_qbs]
qbs_integrableN [lemma, in QBS.probability_qbs]
qbs_integrableB [lemma, in QBS.probability_qbs]
qbs_integrableD [lemma, in QBS.probability_qbs]
qbs_integrable [definition, in QBS.probability_qbs]
qbs_bind_decomp [lemma, in QBS.probability_qbs]
qbs_strength_morphism [lemma, in QBS.probability_qbs]
qbs_join_morphism [lemma, in QBS.probability_qbs]
qbs_strength_return [lemma, in QBS.probability_qbs]
qbs_strength_assoc [lemma, in QBS.probability_qbs]
qbs_strength_unit [lemma, in QBS.probability_qbs]
qbs_strength_natural [lemma, in QBS.probability_qbs]
qbs_bind_equiv_l_return [lemma, in QBS.probability_qbs]
qbs_bind_strong_equiv_l [lemma, in QBS.probability_qbs]
qbs_bind_equiv_l [lemma, in QBS.probability_qbs]
qbs_strength [definition, in QBS.probability_qbs]
qbs_join [definition, in QBS.probability_qbs]
qbs_variance [definition, in QBS.probability_qbs]
qbs_prob_event [definition, in QBS.probability_qbs]
qbs_expect [definition, in QBS.probability_qbs]
qbs_pushforward_integrable [lemma, in QBS.probability_qbs]
qbs_integral_as_pushforward [lemma, in QBS.probability_qbs]
qbs_integral_bind [lemma, in QBS.probability_qbs]
qbs_integral_return [lemma, in QBS.probability_qbs]
qbs_integral_const [lemma, in QBS.probability_qbs]
qbs_integral_equiv_same_alpha [lemma, in QBS.probability_qbs]
qbs_integral_equiv [lemma, in QBS.probability_qbs]
qbs_pushforward_agree [lemma, in QBS.probability_qbs]
qbs_measurable_sigma_Mx [lemma, in QBS.probability_qbs]
qbs_measurable [definition, in QBS.probability_qbs]
qbs_integral [definition, in QBS.probability_qbs]
qbs_bindA [lemma, in QBS.probability_qbs]
qbs_bind_returnr [lemma, in QBS.probability_qbs]
qbs_bind_returnl [lemma, in QBS.probability_qbs]
qbs_bind_morph [lemma, in QBS.probability_qbs]
qbs_bind_strong [definition, in QBS.probability_qbs]
qbs_bind [definition, in QBS.probability_qbs]
qbs_bind_alpha_random_return [lemma, in QBS.probability_qbs]
qbs_bind_alpha_random_const [lemma, in QBS.probability_qbs]
qbs_bind_alpha_random_strong [lemma, in QBS.probability_qbs]
qbs_morphism_strong [definition, in QBS.probability_qbs]
qbs_return_random [lemma, in QBS.probability_qbs]
qbs_return_equiv [lemma, in QBS.probability_qbs]
qbs_return [definition, in QBS.probability_qbs]
qbs_prob_equiv_trans [lemma, in QBS.probability_qbs]
qbs_prob_equivC [lemma, in QBS.probability_qbs]
qbs_prob_equivxx [lemma, in QBS.probability_qbs]
qbs_prob_equiv [definition, in QBS.probability_qbs]
qbs_prob_alpha_random [projection, in QBS.probability_qbs]
qbs_prob_mu [projection, in QBS.probability_qbs]
qbs_prob_alpha [projection, in QBS.probability_qbs]
qbs_prob [record, in QBS.probability_qbs]
qbs_prob_space_qbs [definition, in QBS.qbs_prob_quot]
qbs_prob_quot_qbs_prob_space__canonical__quasi_borel_QBSpace [definition, in QBS.qbs_prob_quot]
qbs_prob_quot.qbs_prob_space_instance.Mx_glue [variable, in QBS.qbs_prob_quot]
qbs_prob_quot.qbs_prob_space_instance.Mx_const [variable, in QBS.qbs_prob_quot]
qbs_prob_quot.qbs_prob_space_instance.Mx_comp [variable, in QBS.qbs_prob_quot]
qbs_prob_quot.qbs_prob_space_instance.Mx [variable, in QBS.qbs_prob_quot]
qbs_prob_quot.qbs_prob_space_instance.X [variable, in QBS.qbs_prob_quot]
qbs_prob_quot.qbs_prob_space_instance [section, in QBS.qbs_prob_quot]
qbs_prob_space [record, in QBS.qbs_prob_quot]
qbs_prob_quot.R [variable, in QBS.qbs_prob_quot]
qbs_prob_quot [section, in QBS.qbs_prob_quot]
qbs_integral_giry [lemma, in QBS.qbs_giry]
qbs_to_giryK [lemma, in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__probability_measure_Probability [definition, in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__probability_measure_SubProbability [definition, in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__measure_function_FiniteMeasure [definition, in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__measure_function_FinNumFun [definition, in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__measure_function_SigmaFiniteMeasure [definition, in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__measure_function_SFiniteMeasure [definition, in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__measure_function_SigmaFiniteContent [definition, in QBS.qbs_giry]
qbs_giry.giry_to_qbs.pf_mu_setT [variable, in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__measure_function_Measure [definition, in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__measure_function_Content [definition, in QBS.qbs_giry]
qbs_giry.giry_to_qbs.pf_mu_sigma_additive [variable, in QBS.qbs_giry]
qbs_giry.giry_to_qbs.pf_mu_ge0 [variable, in QBS.qbs_giry]
qbs_giry.giry_to_qbs.pf_mu0 [variable, in QBS.qbs_giry]
qbs_giry.giry_to_qbs.pf_mu [variable, in QBS.qbs_giry]
qbs_giry.giry_to_qbs.P [variable, in QBS.qbs_giry]
qbs_giry.giry_to_qbs.decode_meas [variable, in QBS.qbs_giry]
qbs_giry.giry_to_qbs.encode_meas [variable, in QBS.qbs_giry]
qbs_giry.giry_to_qbs.decode [variable, in QBS.qbs_giry]
qbs_giry.giry_to_qbs.encode [variable, in QBS.qbs_giry]
qbs_giry.giry_to_qbs.M [variable, in QBS.qbs_giry]
qbs_giry.giry_to_qbs.d [variable, in QBS.qbs_giry]
qbs_giry.giry_to_qbs [section, in QBS.qbs_giry]
qbs_to_giry [definition, in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__probability_measure_Probability [definition, in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__probability_measure_SubProbability [definition, in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__measure_function_FiniteMeasure [definition, in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__measure_function_FinNumFun [definition, in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__measure_function_SigmaFiniteMeasure [definition, in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__measure_function_SFiniteMeasure [definition, in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__measure_function_SigmaFiniteContent [definition, in QBS.qbs_giry]
qbs_to_giry_mu_setT [lemma, in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__measure_function_Measure [definition, in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__measure_function_Content [definition, in QBS.qbs_giry]
qbs_to_giry_mu_semi_sigma_additive [lemma, in QBS.qbs_giry]
qbs_to_giry_mu_ge0 [lemma, in QBS.qbs_giry]
qbs_to_giry_mu0 [lemma, in QBS.qbs_giry]
qbs_to_giry_mu [definition, in QBS.qbs_giry]
qbs_giry.qbs_to_giry.alpha_meas [variable, in QBS.qbs_giry]
qbs_giry.qbs_to_giry.mu [variable, in QBS.qbs_giry]
qbs_giry.qbs_to_giry.alpha [variable, in QBS.qbs_giry]
qbs_giry.qbs_to_giry.p [variable, in QBS.qbs_giry]
qbs_giry.qbs_to_giry.M [variable, in QBS.qbs_giry]
qbs_giry.qbs_to_giry.d [variable, in QBS.qbs_giry]
qbs_giry.qbs_to_giry [section, in QBS.qbs_giry]
qbs_giry.R [variable, in QBS.qbs_giry]
qbs_giry [section, in QBS.qbs_giry]
qbs_prob_pair_measure_eq_bind [lemma, in QBS.pair_qbs_measure]
qbs_pair_integral_comm [lemma, in QBS.pair_qbs_measure]
qbs_variance_indep_sum [lemma, in QBS.pair_qbs_measure]
qbs_pair_variance [definition, in QBS.pair_qbs_measure]
qbs_pair_integral_factorization [lemma, in QBS.pair_qbs_measure]
qbs_indep [definition, in QBS.pair_qbs_measure]
qbs_pair_integral_snd [lemma, in QBS.pair_qbs_measure]
qbs_pair_integral_fst [lemma, in QBS.pair_qbs_measure]
qbs_pair_integral_iterated [lemma, in QBS.pair_qbs_measure]
qbs_pair_fun [definition, in QBS.pair_qbs_measure]
qbs_pair_integral [definition, in QBS.pair_qbs_measure]
qbs_prob_pair [definition, in QBS.pair_qbs_measure]
qbs_pair_alpha_random [lemma, in QBS.pair_qbs_measure]
qbs_pair_mu [definition, in QBS.pair_qbs_measure]
qbs_pair_alpha [definition, in QBS.pair_qbs_measure]
qbs_pair_mu_build [definition, in QBS.pair_qbs_measure]
qbs_quotient.monad_laws_quot.Z [variable, in QBS.qbs_quotient]
qbs_quotient.monad_laws_quot.Y [variable, in QBS.qbs_quotient]
qbs_quotient.monad_laws_quot.X [variable, in QBS.qbs_quotient]
qbs_quotient.monad_laws_quot [section, in QBS.qbs_quotient]
qbs_quotient.well_defined.Y [variable, in QBS.qbs_quotient]
qbs_quotient.well_defined.X [variable, in QBS.qbs_quotient]
qbs_quotient.well_defined [section, in QBS.qbs_quotient]
qbs_quotient.lifted_ops.Y [variable, in QBS.qbs_quotient]
qbs_quotient.lifted_ops.X [variable, in QBS.qbs_quotient]
qbs_quotient.lifted_ops [section, in QBS.qbs_quotient]
qbs_equivE [lemma, in QBS.qbs_quotient]
qbs_equivP [lemma, in QBS.qbs_quotient]
qbs_quotient_qbs_quot__canonical__generic_quotient_EqQuotient [definition, in QBS.qbs_quotient]
qbs_quotient_qbs_quot__canonical__generic_quotient_Quotient [definition, in QBS.qbs_quotient]
qbs_quotient_qbs_quot__canonical__choice_Choice [definition, in QBS.qbs_quotient]
qbs_quotient_qbs_quot__canonical__eqtype_Equality [definition, in QBS.qbs_quotient]
qbs_quot [definition, in QBS.qbs_quotient]
qbs_quotient.quotient_def.X [variable, in QBS.qbs_quotient]
qbs_quotient.quotient_def [section, in QBS.qbs_quotient]
qbs_prob_equivRel [definition, in QBS.qbs_quotient]
qbs_quotient.equiv_instances.qbs_equiv_op_trans [variable, in QBS.qbs_quotient]
qbs_quotient.equiv_instances.qbs_equiv_op_sym [variable, in QBS.qbs_quotient]
qbs_quotient.equiv_instances.qbs_equiv_op_refl [variable, in QBS.qbs_quotient]
qbs_equiv_op [definition, in QBS.qbs_quotient]
qbs_quotient.equiv_instances.X [variable, in QBS.qbs_quotient]
qbs_quotient.equiv_instances [section, in QBS.qbs_quotient]
qbs_quotient.R [variable, in QBS.qbs_quotient]
qbs_quotient [section, in QBS.qbs_quotient]
qbs_expect_normal [lemma, in QBS.measure_as_qbs_measure]
qbs_expect_uniform [lemma, in QBS.measure_as_qbs_measure]
qbs_expect_bernoulli [lemma, in QBS.measure_as_qbs_measure]
qbs_uniform_random [lemma, in QBS.measure_as_qbs_measure]
qbs_normal_morphism [lemma, in QBS.measure_as_qbs_measure]
qbs_uniform [definition, in QBS.measure_as_qbs_measure]
qbs_bernoulli [definition, in QBS.measure_as_qbs_measure]
qbs_normal_distribution [definition, in QBS.measure_as_qbs_measure]
qbs_supT_least [lemma, in QBS.quasi_borel]
qbs_supT_ub_r [lemma, in QBS.quasi_borel]
qbs_supT_ub_l [lemma, in QBS.quasi_borel]
qbs_supT [definition, in QBS.quasi_borel]
qbs_leT_antisym [lemma, in QBS.quasi_borel]
qbs_leT_trans [lemma, in QBS.quasi_borel]
qbs_leT_refl [lemma, in QBS.quasi_borel]
qbs_leT [definition, in QBS.quasi_borel]
qbs_mul [definition, in QBS.quasi_borel]
qbs_add [definition, in QBS.quasi_borel]
qbs_unit [definition, in QBS.quasi_borel]
qbs_morphism_eval_curry [lemma, in QBS.quasi_borel]
qbs_morphism_curry_eval [lemma, in QBS.quasi_borel]
qbs_curry [definition, in QBS.quasi_borel]
qbs_eval [definition, in QBS.quasi_borel]
qbs_pair [definition, in QBS.quasi_borel]
qbs_snd [definition, in QBS.quasi_borel]
qbs_fst [definition, in QBS.quasi_borel]
qbs_Mx_glueT [lemma, in QBS.quasi_borel]
qbs_Mx_compT [lemma, in QBS.quasi_borel]
qbs_const [definition, in QBS.quasi_borel]
qbs_comp [definition, in QBS.quasi_borel]
qbs_id [definition, in QBS.quasi_borel]
qbs_morphism [definition, in QBS.quasi_borel]
qbs_hom_proof [definition, in QBS.quasi_borel]
qbs_Mx_glue [definition, in QBS.quasi_borel]
qbs_Mx_const [definition, in QBS.quasi_borel]
qbs_Mx_comp [definition, in QBS.quasi_borel]
qbs_Mx [definition, in QBS.quasi_borel]
qbs_giry [library]
qbs_prob_quot [library]
qbs_kernel [library]
qbs_quotient [library]
qbs.expQ_instance.Y [variable, in QBS.quasi_borel]
qbs.expQ_instance.X [variable, in QBS.quasi_borel]
qbs.expQ_instance [section, in QBS.quasi_borel]
qbs.generating_qbs_instance.G [variable, in QBS.quasi_borel]
qbs.generating_qbs_instance.T [variable, in QBS.quasi_borel]
qbs.generating_qbs_instance [section, in QBS.quasi_borel]
qbs.prodQ_instance.Y [variable, in QBS.quasi_borel]
qbs.prodQ_instance.X [variable, in QBS.quasi_borel]
qbs.prodQ_instance [section, in QBS.quasi_borel]
qbs.qbs_order.T [variable, in QBS.quasi_borel]
qbs.qbs_order [section, in QBS.quasi_borel]
qbs.qbs_unit_instance.hf [variable, in QBS.quasi_borel]
qbs.qbs_unit_instance.f [variable, in QBS.quasi_borel]
qbs.qbs_unit_instance.X [variable, in QBS.quasi_borel]
qbs.qbs_unit_instance [section, in QBS.quasi_borel]
qbs.qbs_curry_instance.curry_proof [variable, in QBS.quasi_borel]
qbs.qbs_curry_instance.curry_fun [variable, in QBS.quasi_borel]
qbs.qbs_curry_instance.x [variable, in QBS.quasi_borel]
qbs.qbs_curry_instance.f [variable, in QBS.quasi_borel]
qbs.qbs_curry_instance.Z [variable, in QBS.quasi_borel]
qbs.qbs_curry_instance.Y [variable, in QBS.quasi_borel]
qbs.qbs_curry_instance.X [variable, in QBS.quasi_borel]
qbs.qbs_curry_instance [section, in QBS.quasi_borel]
qbs.qbs_eval_instance.hf [variable, in QBS.quasi_borel]
qbs.qbs_eval_instance.f [variable, in QBS.quasi_borel]
qbs.qbs_eval_instance.Y [variable, in QBS.quasi_borel]
qbs.qbs_eval_instance.X [variable, in QBS.quasi_borel]
qbs.qbs_eval_instance [section, in QBS.quasi_borel]
qbs.qbs_pair_instance.hfg [variable, in QBS.quasi_borel]
qbs.qbs_pair_instance.fg [variable, in QBS.quasi_borel]
qbs.qbs_pair_instance.g [variable, in QBS.quasi_borel]
qbs.qbs_pair_instance.f [variable, in QBS.quasi_borel]
qbs.qbs_pair_instance.Y [variable, in QBS.quasi_borel]
qbs.qbs_pair_instance.X [variable, in QBS.quasi_borel]
qbs.qbs_pair_instance.W [variable, in QBS.quasi_borel]
qbs.qbs_pair_instance [section, in QBS.quasi_borel]
qbs.qbs_snd_instance.hf [variable, in QBS.quasi_borel]
qbs.qbs_snd_instance.f [variable, in QBS.quasi_borel]
qbs.qbs_snd_instance.Y [variable, in QBS.quasi_borel]
qbs.qbs_snd_instance.X [variable, in QBS.quasi_borel]
qbs.qbs_snd_instance [section, in QBS.quasi_borel]
qbs.qbs_fst_instance.hf [variable, in QBS.quasi_borel]
qbs.qbs_fst_instance.f [variable, in QBS.quasi_borel]
qbs.qbs_fst_instance.Y [variable, in QBS.quasi_borel]
qbs.qbs_fst_instance.X [variable, in QBS.quasi_borel]
qbs.qbs_fst_instance [section, in QBS.quasi_borel]
qbs.qbs_const_instance.hf [variable, in QBS.quasi_borel]
qbs.qbs_const_instance.f [variable, in QBS.quasi_borel]
qbs.qbs_const_instance.y [variable, in QBS.quasi_borel]
qbs.qbs_const_instance.Y [variable, in QBS.quasi_borel]
qbs.qbs_const_instance.X [variable, in QBS.quasi_borel]
qbs.qbs_const_instance [section, in QBS.quasi_borel]
qbs.qbs_comp_instance.hgf [variable, in QBS.quasi_borel]
qbs.qbs_comp_instance.gf [variable, in QBS.quasi_borel]
qbs.qbs_comp_instance.g [variable, in QBS.quasi_borel]
qbs.qbs_comp_instance.f [variable, in QBS.quasi_borel]
qbs.qbs_comp_instance.Z [variable, in QBS.quasi_borel]
qbs.qbs_comp_instance.Y [variable, in QBS.quasi_borel]
qbs.qbs_comp_instance.X [variable, in QBS.quasi_borel]
qbs.qbs_comp_instance [section, in QBS.quasi_borel]
qbs.qbs_id_instance.hf [variable, in QBS.quasi_borel]
qbs.qbs_id_instance.f [variable, in QBS.quasi_borel]
qbs.qbs_id_instance.X [variable, in QBS.quasi_borel]
qbs.qbs_id_instance [section, in QBS.quasi_borel]
qbs.R [variable, in QBS.quasi_borel]
qbs.R_qbs_instance.ax3 [variable, in QBS.quasi_borel]
qbs.R_qbs_instance.ax2 [variable, in QBS.quasi_borel]
qbs.R_qbs_instance.ax1 [variable, in QBS.quasi_borel]
qbs.R_qbs_instance.Mx [variable, in QBS.quasi_borel]
qbs.R_qbs_instance.M [variable, in QBS.quasi_borel]
qbs.R_qbs_instance.d [variable, in QBS.quasi_borel]
qbs.R_qbs_instance [section, in QBS.quasi_borel]
qbs.sub_qbs_def.sub_Mx [variable, in QBS.quasi_borel]
qbs.sub_qbs_def.sub_proj [variable, in QBS.quasi_borel]
qbs.sub_qbs_def.sub_car [variable, in QBS.quasi_borel]
qbs.sub_qbs_def.P [variable, in QBS.quasi_borel]
qbs.sub_qbs_def.X [variable, in QBS.quasi_borel]
qbs.sub_qbs_def [section, in QBS.quasi_borel]
qbs.unitQ_instance [section, in QBS.quasi_borel]
qps_pick_repr_equiv [lemma, in QBS.qbs_prob_quot]
qps_pick_repr [definition, in QBS.qbs_prob_quot]
qps_integral_bind [lemma, in QBS.qbs_prob_quot]
qps_integral_return [lemma, in QBS.qbs_prob_quot]
qps_integral_const [lemma, in QBS.qbs_prob_quot]
qps_prob_event_equiv [lemma, in QBS.qbs_prob_quot]
qps_prob_event [definition, in QBS.qbs_prob_quot]
qps_expect [definition, in QBS.qbs_prob_quot]
qps_bindA [lemma, in QBS.qbs_prob_quot]
qps_bind_returnr [lemma, in QBS.qbs_prob_quot]
qps_bind_returnl [lemma, in QBS.qbs_prob_quot]
qps_map_equiv [lemma, in QBS.qbs_prob_quot]
qps_integral_equiv [lemma, in QBS.qbs_prob_quot]
qps_return_equiv [lemma, in QBS.qbs_prob_quot]
qps_map [definition, in QBS.qbs_prob_quot]
qps_integral [definition, in QBS.qbs_prob_quot]
qps_bind_strong [definition, in QBS.qbs_prob_quot]
qps_bind [definition, in QBS.qbs_prob_quot]
qps_return [definition, in QBS.qbs_prob_quot]
qps_of [definition, in QBS.qbs_prob_quot]
qps_eq_trans [lemma, in QBS.qbs_prob_quot]
qps_eqC [lemma, in QBS.qbs_prob_quot]
qps_eqxx [lemma, in QBS.qbs_prob_quot]
qps_eq [definition, in QBS.qbs_prob_quot]
qps_repr [projection, in QBS.qbs_prob_quot]
quasi_borel_T__canonical__quasi_borel_QBSpace [definition, in QBS.quasi_borel]
quasi_borel_sub_car__canonical__quasi_borel_QBSpace [definition, in QBS.quasi_borel]
quasi_borel_f__canonical__quasi_borel_QBSHom__31 [definition, in QBS.quasi_borel]
quasi_borel_curry_fun__canonical__quasi_borel_QBSHom [definition, in QBS.quasi_borel]
quasi_borel_f__canonical__quasi_borel_QBSHom__24 [definition, in QBS.quasi_borel]
quasi_borel_fg__canonical__quasi_borel_QBSHom [definition, in QBS.quasi_borel]
quasi_borel_f__canonical__quasi_borel_QBSHom__17 [definition, in QBS.quasi_borel]
quasi_borel_f__canonical__quasi_borel_QBSHom__14 [definition, in QBS.quasi_borel]
quasi_borel_f__canonical__quasi_borel_QBSHom__7 [definition, in QBS.quasi_borel]
quasi_borel_gf__canonical__quasi_borel_QBSHom [definition, in QBS.quasi_borel]
quasi_borel_f__canonical__quasi_borel_QBSHom [definition, in QBS.quasi_borel]
quasi_borel [library]
quot_bind_returnr [lemma, in QBS.qbs_quotient]
quot_bind_returnl [lemma, in QBS.qbs_quotient]
quot_integral_proper [lemma, in QBS.qbs_quotient]
quot_bind_strong_proper [lemma, in QBS.qbs_quotient]
quot_map_proper [lemma, in QBS.qbs_quotient]
quot_return_equiv [lemma, in QBS.qbs_quotient]
quot_bind_strong [definition, in QBS.qbs_quotient]
quot_map [definition, in QBS.qbs_quotient]
quot_integral [definition, in QBS.qbs_quotient]
quot_return [definition, in QBS.qbs_quotient]
quot_reprK [lemma, in QBS.qbs_quotient]
R
realQ [definition, in QBS.quasi_borel]repr_equiv [lemma, in QBS.qbs_quotient]
R_full_faithful_standard_borel [lemma, in QBS.measure_qbs_adjunction]
R_standard_borel [lemma, in QBS.measure_qbs_adjunction]
R_preserves_prod [lemma, in QBS.measure_qbs_adjunction]
R_qbs_comp [lemma, in QBS.measure_qbs_adjunction]
R_qbs_id [lemma, in QBS.measure_qbs_adjunction]
R_qbs_morphism [lemma, in QBS.measure_qbs_adjunction]
R_qbs [definition, in QBS.quasi_borel]
S
sb_retractK [projection, in QBS.measure_qbs_adjunction]sb_decode [projection, in QBS.measure_qbs_adjunction]
sb_encode [projection, in QBS.measure_qbs_adjunction]
scalar_of_s_mul_pdf [lemma, in QBS.showcase.bayesian_regression]
scalar_of_s_eq [lemma, in QBS.showcase.bayesian_regression]
scalar_of_s_ge0 [lemma, in QBS.showcase.bayesian_regression]
scalar_of_s [definition, in QBS.showcase.bayesian_regression]
sigma_Mx_bigcup [lemma, in QBS.quasi_borel]
sigma_Mx_setC [lemma, in QBS.quasi_borel]
sigma_Mx_setT [lemma, in QBS.quasi_borel]
sigma_Mx [definition, in QBS.quasi_borel]
slope_prior [definition, in QBS.showcase.bayesian_regression]
sos_int_proof [lemma, in QBS.showcase.bayesian_regression]
sos_meas_proof [lemma, in QBS.showcase.bayesian_regression]
Specif_sigT__canonical__quasi_borel_QBSpace [definition, in QBS.coproduct_qbs]
sqrtr_nine_div_neq0 [lemma, in QBS.normal_algebra]
sqrtr_pnat_div_neq0 [lemma, in QBS.normal_algebra]
standard_borel_lr_sets_ident [lemma, in QBS.measure_qbs_adjunction]
standard_borel_wit [record, in QBS.measure_qbs_adjunction]
standard_borel_mR.R [variable, in QBS.standard_borel]
standard_borel_mR [section, in QBS.standard_borel]
standard_borel [library]
sub_qbs [definition, in QBS.quasi_borel]
sub_qbs_Mx_glue [lemma, in QBS.quasi_borel]
sub_qbs_Mx_const [lemma, in QBS.quasi_borel]
sub_qbs_Mx_comp [lemma, in QBS.quasi_borel]
T
truncnP [abbreviation, in QBS.measure_qbs_adjunction]U
unitQ [definition, in QBS.quasi_borel]unit_to_pair_snd_le1 [lemma, in QBS.standard_borel]
unit_to_pair_snd_ge0 [lemma, in QBS.standard_borel]
unit_to_pair_fst_le1 [lemma, in QBS.standard_borel]
unit_to_pair_fst_ge0 [lemma, in QBS.standard_borel]
unit_to_pairK [lemma, in QBS.standard_borel]
unit_to_pair [definition, in QBS.standard_borel]
V
variance_prod_snd [lemma, in QBS.pair_qbs_measure]variance_prod_fst [lemma, in QBS.pair_qbs_measure]
var_recurrence [lemma, in QBS.normal_algebra]
Module Index
I
isQBS [in QBS.quasi_borel]isQBSMorphism [in QBS.quasi_borel]
isQBSMorphism.Exports [in QBS.quasi_borel]
isQBS.Exports [in QBS.quasi_borel]
Q
QBSHom [in QBS.quasi_borel]QBSHomElpiOperations [in QBS.quasi_borel]
QBSHom.Exports [in QBS.quasi_borel]
QBSpace [in QBS.quasi_borel]
QBSpaceElpiOperations [in QBS.quasi_borel]
QBSpace.Exports [in QBS.quasi_borel]
Variable Index
B
bayesian_regression.d_pair_meas_tac [in QBS.showcase.bayesian_regression]bayesian_regression.phase1_sigma5 [in QBS.showcase.bayesian_regression]
bayesian_regression.phase1_mu5 [in QBS.showcase.bayesian_regression]
bayesian_regression.noise_sigma [in QBS.showcase.bayesian_regression]
bayesian_regression.prior_sigma [in QBS.showcase.bayesian_regression]
bayesian_regression.R [in QBS.showcase.bayesian_regression]
binary_digit_interleaving.measurability_constructions.step [in QBS.standard_borel]
binary_digit_interleaving.R [in QBS.standard_borel]
C
coproduct_qbs.listQ_instance.ax3 [in QBS.coproduct_qbs]coproduct_qbs.listQ_instance.ax2 [in QBS.coproduct_qbs]
coproduct_qbs.listQ_instance.ax1 [in QBS.coproduct_qbs]
coproduct_qbs.listQ_instance.Mx [in QBS.coproduct_qbs]
coproduct_qbs.listQ_instance.x0 [in QBS.coproduct_qbs]
coproduct_qbs.listQ_instance.X [in QBS.coproduct_qbs]
coproduct_qbs.piQ_instance.ax3 [in QBS.coproduct_qbs]
coproduct_qbs.piQ_instance.ax2 [in QBS.coproduct_qbs]
coproduct_qbs.piQ_instance.ax1 [in QBS.coproduct_qbs]
coproduct_qbs.piQ_instance.Mx [in QBS.coproduct_qbs]
coproduct_qbs.piQ_instance.X [in QBS.coproduct_qbs]
coproduct_qbs.piQ_instance.I [in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance.ax3 [in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance.ax2 [in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance.ax1 [in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance.Mx [in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance.inh [in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance.X [in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance.I [in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance.d [in QBS.coproduct_qbs]
coproduct_qbs.coprodQ_instance.ax3 [in QBS.coproduct_qbs]
coproduct_qbs.coprodQ_instance.ax2 [in QBS.coproduct_qbs]
coproduct_qbs.coprodQ_instance.ax1 [in QBS.coproduct_qbs]
coproduct_qbs.coprodQ_instance.Mx [in QBS.coproduct_qbs]
coproduct_qbs.coprodQ_instance.Y [in QBS.coproduct_qbs]
coproduct_qbs.coprodQ_instance.X [in QBS.coproduct_qbs]
coproduct_qbs.R [in QBS.coproduct_qbs]
I
integral_normal_prob.R [in QBS.showcase.bayesian_regression]isQBSMorphism.isQBSMorphism.f [in QBS.quasi_borel]
isQBSMorphism.isQBSMorphism.R [in QBS.quasi_borel]
isQBSMorphism.isQBSMorphism.X [in QBS.quasi_borel]
isQBSMorphism.isQBSMorphism.Y [in QBS.quasi_borel]
isQBS.isQBS.R [in QBS.quasi_borel]
isQBS.isQBS.T [in QBS.quasi_borel]
M
measure_as_qbs.R [in QBS.measure_as_qbs_measure]mqa.R [in QBS.measure_qbs_adjunction]
N
normal_density_algebra.bayesian_phase2_slope.mu3_s [in QBS.normal_algebra]normal_density_algebra.bayesian_phase2_slope.mu2_s [in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.mu1_s [in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.mu0_s [in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.sigma3 [in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.W45 [in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.sigma2 [in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.W34 [in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.sigma1 [in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.W23 [in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.sigma0 [in QBS.normal_algebra]
normal_density_algebra.bayesian_phase2_slope.W12 [in QBS.normal_algebra]
normal_density_algebra.three_neq0 [in QBS.normal_algebra]
normal_density_algebra.half_neq0 [in QBS.normal_algebra]
normal_density_algebra.R [in QBS.normal_algebra]
P
pair_qbs_measure.pair_mu_build.pf_mu_setT [in QBS.pair_qbs_measure]pair_qbs_measure.pair_mu_build.pf_mu_sigma [in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.pf_mu_ge0 [in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.pf_mu0 [in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.pf_mu [in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.mu_q [in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.mu_p [in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.q [in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.p [in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.Y [in QBS.pair_qbs_measure]
pair_qbs_measure.pair_mu_build.X [in QBS.pair_qbs_measure]
pair_qbs_measure.R [in QBS.pair_qbs_measure]
phi_psi.R [in QBS.standard_borel]
probability_qbs.qbs_normalize_def.X [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.norm_mu_setT [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.norm_mu_sigma [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.norm_mu_ge0 [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.norm_mu0 [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.norm_mu [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.wdiv_meas [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.wdiv_ge0 [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.wdiv [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.ev_r_neq0 [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.ev_r_gt0 [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.ev_r [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.hev_fin [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.hev_pos [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.ev [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.hw_meas [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.hw_ge0 [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.w [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.p [in QBS.probability_qbs]
probability_qbs.normalize_mu_build.X [in QBS.probability_qbs]
probability_qbs.probability_monad.monadP_instance.ax_glue [in QBS.probability_qbs]
probability_qbs.probability_monad.monadP_instance.ax_const [in QBS.probability_qbs]
probability_qbs.probability_monad.monadP_instance.ax_comp [in QBS.probability_qbs]
probability_qbs.probability_monad.monadP_instance.Mx [in QBS.probability_qbs]
probability_qbs.probability_monad.monadP_instance.X [in QBS.probability_qbs]
probability_qbs.R [in QBS.probability_qbs]
Q
qbs_kernel.round_trip.decode_encode [in QBS.qbs_kernel]qbs_kernel.round_trip.decode_meas [in QBS.qbs_kernel]
qbs_kernel.round_trip.encode_meas [in QBS.qbs_kernel]
qbs_kernel.round_trip.decode [in QBS.qbs_kernel]
qbs_kernel.round_trip.encode [in QBS.qbs_kernel]
qbs_kernel.round_trip.M [in QBS.qbs_kernel]
qbs_kernel.round_trip.d [in QBS.qbs_kernel]
qbs_kernel.integration.M [in QBS.qbs_kernel]
qbs_kernel.integration.d [in QBS.qbs_kernel]
qbs_kernel.bind_return.M2 [in QBS.qbs_kernel]
qbs_kernel.bind_return.M1 [in QBS.qbs_kernel]
qbs_kernel.bind_return.d2 [in QBS.qbs_kernel]
qbs_kernel.bind_return.d1 [in QBS.qbs_kernel]
qbs_kernel.dirac_comp.M2 [in QBS.qbs_kernel]
qbs_kernel.dirac_comp.M1 [in QBS.qbs_kernel]
qbs_kernel.dirac_comp.d2 [in QBS.qbs_kernel]
qbs_kernel.dirac_comp.d1 [in QBS.qbs_kernel]
qbs_kernel.giry_pushforward.M2 [in QBS.qbs_kernel]
qbs_kernel.giry_pushforward.M1 [in QBS.qbs_kernel]
qbs_kernel.giry_pushforward.d2 [in QBS.qbs_kernel]
qbs_kernel.giry_pushforward.d1 [in QBS.qbs_kernel]
qbs_kernel.equiv_kernel.M [in QBS.qbs_kernel]
qbs_kernel.equiv_kernel.d [in QBS.qbs_kernel]
qbs_kernel.const_kernel.M [in QBS.qbs_kernel]
qbs_kernel.const_kernel.d [in QBS.qbs_kernel]
qbs_kernel.kdirac_measurability.M2 [in QBS.qbs_kernel]
qbs_kernel.kdirac_measurability.M1 [in QBS.qbs_kernel]
qbs_kernel.kdirac_measurability.d2 [in QBS.qbs_kernel]
qbs_kernel.kdirac_measurability.d1 [in QBS.qbs_kernel]
qbs_kernel.qbs_morph_kernel.sb2 [in QBS.qbs_kernel]
qbs_kernel.qbs_morph_kernel.sb1 [in QBS.qbs_kernel]
qbs_kernel.qbs_morph_kernel.M2 [in QBS.qbs_kernel]
qbs_kernel.qbs_morph_kernel.M1 [in QBS.qbs_kernel]
qbs_kernel.qbs_morph_kernel.d2 [in QBS.qbs_kernel]
qbs_kernel.qbs_morph_kernel.d1 [in QBS.qbs_kernel]
qbs_kernel.qbs_return_dirac.decode_encode [in QBS.qbs_kernel]
qbs_kernel.qbs_return_dirac.decode_meas [in QBS.qbs_kernel]
qbs_kernel.qbs_return_dirac.encode_meas [in QBS.qbs_kernel]
qbs_kernel.qbs_return_dirac.decode [in QBS.qbs_kernel]
qbs_kernel.qbs_return_dirac.encode [in QBS.qbs_kernel]
qbs_kernel.qbs_return_dirac.M [in QBS.qbs_kernel]
qbs_kernel.qbs_return_dirac.d [in QBS.qbs_kernel]
qbs_kernel.kdirac_unfold.M2 [in QBS.qbs_kernel]
qbs_kernel.kdirac_unfold.M1 [in QBS.qbs_kernel]
qbs_kernel.kdirac_unfold.d2 [in QBS.qbs_kernel]
qbs_kernel.kdirac_unfold.d1 [in QBS.qbs_kernel]
qbs_kernel.pushforward_prob.M2 [in QBS.qbs_kernel]
qbs_kernel.pushforward_prob.M1 [in QBS.qbs_kernel]
qbs_kernel.pushforward_prob.d2 [in QBS.qbs_kernel]
qbs_kernel.pushforward_prob.d1 [in QBS.qbs_kernel]
qbs_kernel.R [in QBS.qbs_kernel]
qbs_prob_quot.qbs_prob_space_instance.Mx_glue [in QBS.qbs_prob_quot]
qbs_prob_quot.qbs_prob_space_instance.Mx_const [in QBS.qbs_prob_quot]
qbs_prob_quot.qbs_prob_space_instance.Mx_comp [in QBS.qbs_prob_quot]
qbs_prob_quot.qbs_prob_space_instance.Mx [in QBS.qbs_prob_quot]
qbs_prob_quot.qbs_prob_space_instance.X [in QBS.qbs_prob_quot]
qbs_prob_quot.R [in QBS.qbs_prob_quot]
qbs_giry.giry_to_qbs.pf_mu_setT [in QBS.qbs_giry]
qbs_giry.giry_to_qbs.pf_mu_sigma_additive [in QBS.qbs_giry]
qbs_giry.giry_to_qbs.pf_mu_ge0 [in QBS.qbs_giry]
qbs_giry.giry_to_qbs.pf_mu0 [in QBS.qbs_giry]
qbs_giry.giry_to_qbs.pf_mu [in QBS.qbs_giry]
qbs_giry.giry_to_qbs.P [in QBS.qbs_giry]
qbs_giry.giry_to_qbs.decode_meas [in QBS.qbs_giry]
qbs_giry.giry_to_qbs.encode_meas [in QBS.qbs_giry]
qbs_giry.giry_to_qbs.decode [in QBS.qbs_giry]
qbs_giry.giry_to_qbs.encode [in QBS.qbs_giry]
qbs_giry.giry_to_qbs.M [in QBS.qbs_giry]
qbs_giry.giry_to_qbs.d [in QBS.qbs_giry]
qbs_giry.qbs_to_giry.alpha_meas [in QBS.qbs_giry]
qbs_giry.qbs_to_giry.mu [in QBS.qbs_giry]
qbs_giry.qbs_to_giry.alpha [in QBS.qbs_giry]
qbs_giry.qbs_to_giry.p [in QBS.qbs_giry]
qbs_giry.qbs_to_giry.M [in QBS.qbs_giry]
qbs_giry.qbs_to_giry.d [in QBS.qbs_giry]
qbs_giry.R [in QBS.qbs_giry]
qbs_quotient.monad_laws_quot.Z [in QBS.qbs_quotient]
qbs_quotient.monad_laws_quot.Y [in QBS.qbs_quotient]
qbs_quotient.monad_laws_quot.X [in QBS.qbs_quotient]
qbs_quotient.well_defined.Y [in QBS.qbs_quotient]
qbs_quotient.well_defined.X [in QBS.qbs_quotient]
qbs_quotient.lifted_ops.Y [in QBS.qbs_quotient]
qbs_quotient.lifted_ops.X [in QBS.qbs_quotient]
qbs_quotient.quotient_def.X [in QBS.qbs_quotient]
qbs_quotient.equiv_instances.qbs_equiv_op_trans [in QBS.qbs_quotient]
qbs_quotient.equiv_instances.qbs_equiv_op_sym [in QBS.qbs_quotient]
qbs_quotient.equiv_instances.qbs_equiv_op_refl [in QBS.qbs_quotient]
qbs_quotient.equiv_instances.X [in QBS.qbs_quotient]
qbs_quotient.R [in QBS.qbs_quotient]
qbs.expQ_instance.Y [in QBS.quasi_borel]
qbs.expQ_instance.X [in QBS.quasi_borel]
qbs.generating_qbs_instance.G [in QBS.quasi_borel]
qbs.generating_qbs_instance.T [in QBS.quasi_borel]
qbs.prodQ_instance.Y [in QBS.quasi_borel]
qbs.prodQ_instance.X [in QBS.quasi_borel]
qbs.qbs_order.T [in QBS.quasi_borel]
qbs.qbs_unit_instance.hf [in QBS.quasi_borel]
qbs.qbs_unit_instance.f [in QBS.quasi_borel]
qbs.qbs_unit_instance.X [in QBS.quasi_borel]
qbs.qbs_curry_instance.curry_proof [in QBS.quasi_borel]
qbs.qbs_curry_instance.curry_fun [in QBS.quasi_borel]
qbs.qbs_curry_instance.x [in QBS.quasi_borel]
qbs.qbs_curry_instance.f [in QBS.quasi_borel]
qbs.qbs_curry_instance.Z [in QBS.quasi_borel]
qbs.qbs_curry_instance.Y [in QBS.quasi_borel]
qbs.qbs_curry_instance.X [in QBS.quasi_borel]
qbs.qbs_eval_instance.hf [in QBS.quasi_borel]
qbs.qbs_eval_instance.f [in QBS.quasi_borel]
qbs.qbs_eval_instance.Y [in QBS.quasi_borel]
qbs.qbs_eval_instance.X [in QBS.quasi_borel]
qbs.qbs_pair_instance.hfg [in QBS.quasi_borel]
qbs.qbs_pair_instance.fg [in QBS.quasi_borel]
qbs.qbs_pair_instance.g [in QBS.quasi_borel]
qbs.qbs_pair_instance.f [in QBS.quasi_borel]
qbs.qbs_pair_instance.Y [in QBS.quasi_borel]
qbs.qbs_pair_instance.X [in QBS.quasi_borel]
qbs.qbs_pair_instance.W [in QBS.quasi_borel]
qbs.qbs_snd_instance.hf [in QBS.quasi_borel]
qbs.qbs_snd_instance.f [in QBS.quasi_borel]
qbs.qbs_snd_instance.Y [in QBS.quasi_borel]
qbs.qbs_snd_instance.X [in QBS.quasi_borel]
qbs.qbs_fst_instance.hf [in QBS.quasi_borel]
qbs.qbs_fst_instance.f [in QBS.quasi_borel]
qbs.qbs_fst_instance.Y [in QBS.quasi_borel]
qbs.qbs_fst_instance.X [in QBS.quasi_borel]
qbs.qbs_const_instance.hf [in QBS.quasi_borel]
qbs.qbs_const_instance.f [in QBS.quasi_borel]
qbs.qbs_const_instance.y [in QBS.quasi_borel]
qbs.qbs_const_instance.Y [in QBS.quasi_borel]
qbs.qbs_const_instance.X [in QBS.quasi_borel]
qbs.qbs_comp_instance.hgf [in QBS.quasi_borel]
qbs.qbs_comp_instance.gf [in QBS.quasi_borel]
qbs.qbs_comp_instance.g [in QBS.quasi_borel]
qbs.qbs_comp_instance.f [in QBS.quasi_borel]
qbs.qbs_comp_instance.Z [in QBS.quasi_borel]
qbs.qbs_comp_instance.Y [in QBS.quasi_borel]
qbs.qbs_comp_instance.X [in QBS.quasi_borel]
qbs.qbs_id_instance.hf [in QBS.quasi_borel]
qbs.qbs_id_instance.f [in QBS.quasi_borel]
qbs.qbs_id_instance.X [in QBS.quasi_borel]
qbs.R [in QBS.quasi_borel]
qbs.R_qbs_instance.ax3 [in QBS.quasi_borel]
qbs.R_qbs_instance.ax2 [in QBS.quasi_borel]
qbs.R_qbs_instance.ax1 [in QBS.quasi_borel]
qbs.R_qbs_instance.Mx [in QBS.quasi_borel]
qbs.R_qbs_instance.M [in QBS.quasi_borel]
qbs.R_qbs_instance.d [in QBS.quasi_borel]
qbs.sub_qbs_def.sub_Mx [in QBS.quasi_borel]
qbs.sub_qbs_def.sub_proj [in QBS.quasi_borel]
qbs.sub_qbs_def.sub_car [in QBS.quasi_borel]
qbs.sub_qbs_def.P [in QBS.quasi_borel]
qbs.sub_qbs_def.X [in QBS.quasi_borel]
S
standard_borel_mR.R [in QBS.standard_borel]Library Index
B
bayesian_regressionC
coproduct_qbsM
measure_qbs_adjunctionmeasure_as_qbs_measure
N
normal_algebraP
pair_qbs_measureprobability_qbs
Q
qbs_giryqbs_prob_quot
qbs_kernel
qbs_quotient
quasi_borel
S
standard_borelLemma Index
A
adjunction_counit [in QBS.measure_qbs_adjunction]adjunction_unit [in QBS.measure_qbs_adjunction]
as_qbs_prob_recover_full [in QBS.measure_as_qbs_measure]
as_qbs_prob_recover [in QBS.measure_as_qbs_measure]
B
bin_sum_has_one_gt0 [in QBS.standard_borel]bin_digit_iter [in QBS.standard_borel]
bin_digits_bin_sum [in QBS.standard_borel]
bin_sum_shift [in QBS.standard_borel]
bin_sum_no_trailing_lt1 [in QBS.standard_borel]
bin_digits_no_trailing_ones [in QBS.standard_borel]
bin_sum_ext [in QBS.standard_borel]
bin_digits_reconstruction [in QBS.standard_borel]
bin_sum_ge0 [in QBS.standard_borel]
bin_sum_le1 [in QBS.standard_borel]
bin_partial_sum_nd [in QBS.standard_borel]
bin_partial_sum_ge0 [in QBS.standard_borel]
bin_partial_sum_le1 [in QBS.standard_borel]
bool_standard_borel [in QBS.measure_qbs_adjunction]
C
complete_the_square [in QBS.normal_algebra]const_kernel_of_qbs_measurable [in QBS.qbs_kernel]
coprodQ_Mx_glue [in QBS.coproduct_qbs]
coprodQ_Mx_const [in QBS.coproduct_qbs]
coprodQ_Mx_comp [in QBS.coproduct_qbs]
D
decode_RRK [in QBS.standard_borel]deinterleave_interleaveK_odd [in QBS.standard_borel]
deinterleave_interleaveK_even [in QBS.standard_borel]
d_le_peak [in QBS.showcase.bayesian_regression]
d_ge0 [in QBS.showcase.bayesian_regression]
E
encode_decode_kcomp_noparam [in QBS.qbs_kernel]encode_RR_mRK [in QBS.standard_borel]
encode_RRK [in QBS.standard_borel]
ereal_standard_borel [in QBS.measure_qbs_adjunction]
evidence_pos [in QBS.showcase.bayesian_regression]
evidence_value [in QBS.showcase.bayesian_regression]
evidence_eq [in QBS.showcase.bayesian_regression]
evidence_ge0 [in QBS.showcase.bayesian_regression]
expectation_prod_indep [in QBS.pair_qbs_measure]
expectation_prod_snd [in QBS.pair_qbs_measure]
expectation_prod_fst [in QBS.pair_qbs_measure]
expQ_Mx_glue [in QBS.quasi_borel]
expQ_Mx_const [in QBS.quasi_borel]
expQ_Mx_comp [in QBS.quasi_borel]
G
gaussian_prod_scalar_gt0 [in QBS.normal_algebra]gaussian_prod_sigma_neq0 [in QBS.normal_algebra]
gaussian_prod_sigma_sqr [in QBS.normal_algebra]
generating_qbs_least [in QBS.quasi_borel]
generating_qbs_incl [in QBS.quasi_borel]
gen_coprodQ_Mx_glue [in QBS.coproduct_qbs]
gen_coprodQ_Mx_const [in QBS.coproduct_qbs]
gen_coprodQ_Mx_comp [in QBS.coproduct_qbs]
geom_half_sum [in QBS.standard_borel]
giry_to_qbsK [in QBS.qbs_giry]
H
half2 [in QBS.standard_borel]I
integral_normal_prob [in QBS.showcase.bayesian_regression]integral_normal_prob [in QBS.measure_as_qbs_measure]
interleave_no_trailing_ones [in QBS.standard_borel]
interleave_deinterleaveK [in QBS.standard_borel]
inv_cvg_approx [in QBS.standard_borel]
is_cvg_bin_partial_sum [in QBS.standard_borel]
K
kdiracE [in QBS.qbs_kernel]kdirac_round_trip [in QBS.qbs_kernel]
kdirac_comp_noparam [in QBS.qbs_kernel]
kdirac_comp [in QBS.qbs_kernel]
kdirac_measurable_kernel [in QBS.qbs_kernel]
kernel_round_trip [in QBS.qbs_kernel]
kernel_integration [in QBS.qbs_kernel]
L
likelihood_single_strong [in QBS.showcase.bayesian_regression]likelihood_single_morphism [in QBS.showcase.bayesian_regression]
listQ_nth_random [in QBS.coproduct_qbs]
listQ_Mx_glue [in QBS.coproduct_qbs]
listQ_Mx_const [in QBS.coproduct_qbs]
listQ_Mx_comp [in QBS.coproduct_qbs]
lr_adj_iff [in QBS.measure_qbs_adjunction]
lr_adj_r2l [in QBS.measure_qbs_adjunction]
lr_adj_l2r [in QBS.measure_qbs_adjunction]
L_qbs_comp [in QBS.measure_qbs_adjunction]
L_qbs_id [in QBS.measure_qbs_adjunction]
L_qbs_morph [in QBS.measure_qbs_adjunction]
L_sigma_bigcup [in QBS.measure_qbs_adjunction]
L_sigma_setC [in QBS.measure_qbs_adjunction]
L_sigma_setT [in QBS.measure_qbs_adjunction]
L_sigma_set0 [in QBS.measure_qbs_adjunction]
M
map_qbs_morph_from [in QBS.quasi_borel]map_qbs_morphism_out [in QBS.quasi_borel]
map_qbs_sub [in QBS.quasi_borel]
map_qbs_random [in QBS.quasi_borel]
measfun_kernel_prob [in QBS.qbs_kernel]
measurable_contract [in QBS.measure_qbs_adjunction]
measurable_contract_fin [in QBS.measure_qbs_adjunction]
measurable_truncn [in QBS.measure_qbs_adjunction]
measurable_fun_nat_discrete [in QBS.measure_qbs_adjunction]
measurable_glue [in QBS.quasi_borel]
measurable_R_to_RR [in QBS.standard_borel]
measurable_RR_to_R [in QBS.standard_borel]
measurable_decode_RR [in QBS.standard_borel]
measurable_psi_setT [in QBS.standard_borel]
measurable_encode_RR [in QBS.standard_borel]
measurable_unit_to_pair_snd [in QBS.standard_borel]
measurable_unit_to_pair_fst [in QBS.standard_borel]
measurable_pair_to_unit [in QBS.standard_borel]
measurable_bool_scale [in QBS.standard_borel]
measurable_deinterleave_odd_digit [in QBS.standard_borel]
measurable_deinterleave_even_digit [in QBS.standard_borel]
measurable_interleave_digit [in QBS.standard_borel]
measurable_bin_digit [in QBS.standard_borel]
measurable_iter_step [in QBS.standard_borel]
measurable_step [in QBS.standard_borel]
measurable_psi [in QBS.standard_borel]
measurable_phi [in QBS.standard_borel]
monadP_map_comp [in QBS.probability_qbs]
monadP_map_id [in QBS.probability_qbs]
monadP_map_morph [in QBS.probability_qbs]
monadP_glue [in QBS.probability_qbs]
monadP_const [in QBS.probability_qbs]
monadP_comp [in QBS.probability_qbs]
monadP_random_impl [in QBS.probability_qbs]
N
nat_standard_borel [in QBS.measure_qbs_adjunction]nine_div_gt0 [in QBS.normal_algebra]
noise_sigma_neq0 [in QBS.showcase.bayesian_regression]
normalize_alpha_random [in QBS.probability_qbs]
normal_pdf_recenter [in QBS.normal_algebra]
normal_fun_linear [in QBS.normal_algebra]
normal_fun_sub [in QBS.normal_algebra]
normal_fun_sym [in QBS.normal_algebra]
normal_pdf_times_chain [in QBS.normal_algebra]
normal_pdf_times' [in QBS.normal_algebra]
normal_pdf_times [in QBS.normal_algebra]
norm_qbs_none [in QBS.showcase.bayesian_regression]
norm_qbs_some [in QBS.showcase.bayesian_regression]
no_trailing_ones_shift [in QBS.standard_borel]
O
obs_product_integrable [in QBS.showcase.bayesian_regression]obs_int_proof [in QBS.showcase.bayesian_regression]
obs_meas_proof [in QBS.showcase.bayesian_regression]
obs_ub [in QBS.showcase.bayesian_regression]
obs_ge0 [in QBS.showcase.bayesian_regression]
obs_rewrite [in QBS.normal_algebra]
P
pair_standard_borel [in QBS.standard_borel]pair_to_unit_phi_in_01 [in QBS.standard_borel]
pair_to_unit_phi_in_itv [in QBS.standard_borel]
pair_to_unit_phi_lt1 [in QBS.standard_borel]
pair_to_unit_phi_gt0 [in QBS.standard_borel]
pair_to_unitK [in QBS.standard_borel]
phase1_integration [in QBS.showcase.bayesian_regression]
phase1_combine5 [in QBS.normal_algebra]
phase1_combine3 [in QBS.normal_algebra]
phase1_sqrtr_var5_neq0 [in QBS.normal_algebra]
phase1_sqrtr_var4_neq0 [in QBS.normal_algebra]
phase1_sqrtr_var3_neq0 [in QBS.normal_algebra]
phase1_sqrtr_var2_neq0 [in QBS.normal_algebra]
phase1_sqrtr_var1_neq0 [in QBS.normal_algebra]
phase1_step45_mu [in QBS.normal_algebra]
phase1_step45_sigma2 [in QBS.normal_algebra]
phase1_step34_mu [in QBS.normal_algebra]
phase1_step34_sigma2 [in QBS.normal_algebra]
phase1_step23_mu [in QBS.normal_algebra]
phase1_step23_sigma2 [in QBS.normal_algebra]
phase1_step12_mu [in QBS.normal_algebra]
phase1_step12_sigma2 [in QBS.normal_algebra]
phase1_step01_mu [in QBS.normal_algebra]
phase1_step01_sigma2 [in QBS.normal_algebra]
phase2_integration [in QBS.showcase.bayesian_regression]
phase2_combine5 [in QBS.normal_algebra]
phase2_const_gt0 [in QBS.normal_algebra]
phase2_final_sigma_neq0 [in QBS.normal_algebra]
phase2_step4_sigma_neq0 [in QBS.normal_algebra]
phase2_step4 [in QBS.normal_algebra]
phase2_scalar45E [in QBS.normal_algebra]
phase2_W45_neq0 [in QBS.normal_algebra]
phase2_scalar45_fun [in QBS.normal_algebra]
phase2_S45 [in QBS.normal_algebra]
phase2_step3_sigma_neq0 [in QBS.normal_algebra]
phase2_step3 [in QBS.normal_algebra]
phase2_scalar34E [in QBS.normal_algebra]
phase2_W34_neq0 [in QBS.normal_algebra]
phase2_scalar34_fun [in QBS.normal_algebra]
phase2_S34 [in QBS.normal_algebra]
phase2_step2_sigma_neq0 [in QBS.normal_algebra]
phase2_step2 [in QBS.normal_algebra]
phase2_scalar23E [in QBS.normal_algebra]
phase2_W23_neq0 [in QBS.normal_algebra]
phase2_scalar23_fun [in QBS.normal_algebra]
phase2_S23 [in QBS.normal_algebra]
phase2_step1_sigma_neq0 [in QBS.normal_algebra]
phase2_step1_sigma2 [in QBS.normal_algebra]
phase2_step1 [in QBS.normal_algebra]
phase2_scalar12E [in QBS.normal_algebra]
phase2_W12_neq0 [in QBS.normal_algebra]
phase2_scalar12_fun [in QBS.normal_algebra]
phase2_S12 [in QBS.normal_algebra]
phase2_step0_sigma_neq0 [in QBS.normal_algebra]
phase2_step0_sigma2 [in QBS.normal_algebra]
phase2_step0 [in QBS.normal_algebra]
phase2_scalar01E [in QBS.normal_algebra]
phase2_scalar45_diff [in QBS.normal_algebra]
phase2_scalar34_diff [in QBS.normal_algebra]
phase2_scalar23_diff [in QBS.normal_algebra]
phase2_scalar12_diff [in QBS.normal_algebra]
phase2_scalar01_fun [in QBS.normal_algebra]
phase2_scalar01_diff [in QBS.normal_algebra]
phiK [in QBS.standard_borel]
phi_has_true_digit [in QBS.standard_borel]
phi_in_01 [in QBS.standard_borel]
phi_ge0 [in QBS.standard_borel]
phi_lt1 [in QBS.standard_borel]
phi_gt0 [in QBS.standard_borel]
piQ_Mx_glue [in QBS.coproduct_qbs]
piQ_Mx_const [in QBS.coproduct_qbs]
piQ_Mx_comp [in QBS.coproduct_qbs]
posterior_measure_characterization [in QBS.showcase.bayesian_regression]
posterior_density_eq [in QBS.showcase.bayesian_regression]
posterior_density_total [in QBS.showcase.bayesian_regression]
predictive_marginal [in QBS.showcase.bayesian_regression]
prior_bind_diag [in QBS.showcase.bayesian_regression]
prior_inner_diag [in QBS.showcase.bayesian_regression]
prior_sigma_gt0 [in QBS.showcase.bayesian_regression]
probability_fin_num_fun [in QBS.qbs_kernel]
prob_sfinite_measure [in QBS.qbs_kernel]
prodQ_random_const [in QBS.quasi_borel]
prodQ_const_random [in QBS.quasi_borel]
prodQ_Mx_glue [in QBS.quasi_borel]
prodQ_Mx_const [in QBS.quasi_borel]
prodQ_Mx_comp [in QBS.quasi_borel]
prod_standard_borel [in QBS.measure_qbs_adjunction]
program_integrates_to_1 [in QBS.showcase.bayesian_regression]
program_succeeds [in QBS.showcase.bayesian_regression]
psiK [in QBS.standard_borel]
pushforward_probability [in QBS.qbs_kernel]
Q
qbs_morphism_length [in QBS.coproduct_qbs]qbs_morphism_gen_to_coprod [in QBS.coproduct_qbs]
qbs_morphism_coprod_to_gen [in QBS.coproduct_qbs]
qbs_morphism_tuple [in QBS.coproduct_qbs]
qbs_morphism_proj [in QBS.coproduct_qbs]
qbs_morphism_gen_inj [in QBS.coproduct_qbs]
qbs_coprod_eta [in QBS.coproduct_qbs]
qbs_morphism_case_inr [in QBS.coproduct_qbs]
qbs_morphism_case_inl [in QBS.coproduct_qbs]
qbs_morphism_case [in QBS.coproduct_qbs]
qbs_morphism_inr [in QBS.coproduct_qbs]
qbs_morphism_inl [in QBS.coproduct_qbs]
qbs_bind_return_map [in QBS.qbs_kernel]
qbs_giry_pushforward [in QBS.qbs_kernel]
qbs_to_giry_map [in QBS.qbs_kernel]
qbs_prob_equiv_giry [in QBS.qbs_kernel]
qbs_morph_kdirac_prob [in QBS.qbs_kernel]
qbs_morph_measurable [in QBS.qbs_kernel]
qbs_return_to_dirac [in QBS.qbs_kernel]
qbs_prob_sfinite [in QBS.qbs_kernel]
qbs_normalize_integral [in QBS.probability_qbs]
qbs_normalize_total [in QBS.probability_qbs]
qbs_normalize_alpha [in QBS.probability_qbs]
qbs_strength_law4 [in QBS.probability_qbs]
qbs_strength_law4_diag [in QBS.probability_qbs]
qbs_chebyshev [in QBS.probability_qbs]
qbs_markov [in QBS.probability_qbs]
qbs_varianceZ [in QBS.probability_qbs]
qbs_varianceE [in QBS.probability_qbs]
qbs_integralZl [in QBS.probability_qbs]
qbs_integralB [in QBS.probability_qbs]
qbs_integralD [in QBS.probability_qbs]
qbs_integrableZl [in QBS.probability_qbs]
qbs_integrableN [in QBS.probability_qbs]
qbs_integrableB [in QBS.probability_qbs]
qbs_integrableD [in QBS.probability_qbs]
qbs_bind_decomp [in QBS.probability_qbs]
qbs_strength_morphism [in QBS.probability_qbs]
qbs_join_morphism [in QBS.probability_qbs]
qbs_strength_return [in QBS.probability_qbs]
qbs_strength_assoc [in QBS.probability_qbs]
qbs_strength_unit [in QBS.probability_qbs]
qbs_strength_natural [in QBS.probability_qbs]
qbs_bind_equiv_l_return [in QBS.probability_qbs]
qbs_bind_strong_equiv_l [in QBS.probability_qbs]
qbs_bind_equiv_l [in QBS.probability_qbs]
qbs_pushforward_integrable [in QBS.probability_qbs]
qbs_integral_as_pushforward [in QBS.probability_qbs]
qbs_integral_bind [in QBS.probability_qbs]
qbs_integral_return [in QBS.probability_qbs]
qbs_integral_const [in QBS.probability_qbs]
qbs_integral_equiv_same_alpha [in QBS.probability_qbs]
qbs_integral_equiv [in QBS.probability_qbs]
qbs_pushforward_agree [in QBS.probability_qbs]
qbs_measurable_sigma_Mx [in QBS.probability_qbs]
qbs_bindA [in QBS.probability_qbs]
qbs_bind_returnr [in QBS.probability_qbs]
qbs_bind_returnl [in QBS.probability_qbs]
qbs_bind_morph [in QBS.probability_qbs]
qbs_bind_alpha_random_return [in QBS.probability_qbs]
qbs_bind_alpha_random_const [in QBS.probability_qbs]
qbs_bind_alpha_random_strong [in QBS.probability_qbs]
qbs_return_random [in QBS.probability_qbs]
qbs_return_equiv [in QBS.probability_qbs]
qbs_prob_equiv_trans [in QBS.probability_qbs]
qbs_prob_equivC [in QBS.probability_qbs]
qbs_prob_equivxx [in QBS.probability_qbs]
qbs_integral_giry [in QBS.qbs_giry]
qbs_to_giryK [in QBS.qbs_giry]
qbs_to_giry_mu_setT [in QBS.qbs_giry]
qbs_to_giry_mu_semi_sigma_additive [in QBS.qbs_giry]
qbs_to_giry_mu_ge0 [in QBS.qbs_giry]
qbs_to_giry_mu0 [in QBS.qbs_giry]
qbs_prob_pair_measure_eq_bind [in QBS.pair_qbs_measure]
qbs_pair_integral_comm [in QBS.pair_qbs_measure]
qbs_variance_indep_sum [in QBS.pair_qbs_measure]
qbs_pair_integral_factorization [in QBS.pair_qbs_measure]
qbs_pair_integral_snd [in QBS.pair_qbs_measure]
qbs_pair_integral_fst [in QBS.pair_qbs_measure]
qbs_pair_integral_iterated [in QBS.pair_qbs_measure]
qbs_pair_alpha_random [in QBS.pair_qbs_measure]
qbs_equivE [in QBS.qbs_quotient]
qbs_equivP [in QBS.qbs_quotient]
qbs_expect_normal [in QBS.measure_as_qbs_measure]
qbs_expect_uniform [in QBS.measure_as_qbs_measure]
qbs_expect_bernoulli [in QBS.measure_as_qbs_measure]
qbs_uniform_random [in QBS.measure_as_qbs_measure]
qbs_normal_morphism [in QBS.measure_as_qbs_measure]
qbs_supT_least [in QBS.quasi_borel]
qbs_supT_ub_r [in QBS.quasi_borel]
qbs_supT_ub_l [in QBS.quasi_borel]
qbs_leT_antisym [in QBS.quasi_borel]
qbs_leT_trans [in QBS.quasi_borel]
qbs_leT_refl [in QBS.quasi_borel]
qbs_morphism_eval_curry [in QBS.quasi_borel]
qbs_morphism_curry_eval [in QBS.quasi_borel]
qbs_Mx_glueT [in QBS.quasi_borel]
qbs_Mx_compT [in QBS.quasi_borel]
qps_pick_repr_equiv [in QBS.qbs_prob_quot]
qps_integral_bind [in QBS.qbs_prob_quot]
qps_integral_return [in QBS.qbs_prob_quot]
qps_integral_const [in QBS.qbs_prob_quot]
qps_prob_event_equiv [in QBS.qbs_prob_quot]
qps_bindA [in QBS.qbs_prob_quot]
qps_bind_returnr [in QBS.qbs_prob_quot]
qps_bind_returnl [in QBS.qbs_prob_quot]
qps_map_equiv [in QBS.qbs_prob_quot]
qps_integral_equiv [in QBS.qbs_prob_quot]
qps_return_equiv [in QBS.qbs_prob_quot]
qps_eq_trans [in QBS.qbs_prob_quot]
qps_eqC [in QBS.qbs_prob_quot]
qps_eqxx [in QBS.qbs_prob_quot]
quot_bind_returnr [in QBS.qbs_quotient]
quot_bind_returnl [in QBS.qbs_quotient]
quot_integral_proper [in QBS.qbs_quotient]
quot_bind_strong_proper [in QBS.qbs_quotient]
quot_map_proper [in QBS.qbs_quotient]
quot_return_equiv [in QBS.qbs_quotient]
quot_reprK [in QBS.qbs_quotient]
R
repr_equiv [in QBS.qbs_quotient]R_full_faithful_standard_borel [in QBS.measure_qbs_adjunction]
R_standard_borel [in QBS.measure_qbs_adjunction]
R_preserves_prod [in QBS.measure_qbs_adjunction]
R_qbs_comp [in QBS.measure_qbs_adjunction]
R_qbs_id [in QBS.measure_qbs_adjunction]
R_qbs_morphism [in QBS.measure_qbs_adjunction]
S
scalar_of_s_mul_pdf [in QBS.showcase.bayesian_regression]scalar_of_s_eq [in QBS.showcase.bayesian_regression]
scalar_of_s_ge0 [in QBS.showcase.bayesian_regression]
sigma_Mx_bigcup [in QBS.quasi_borel]
sigma_Mx_setC [in QBS.quasi_borel]
sigma_Mx_setT [in QBS.quasi_borel]
sos_int_proof [in QBS.showcase.bayesian_regression]
sos_meas_proof [in QBS.showcase.bayesian_regression]
sqrtr_nine_div_neq0 [in QBS.normal_algebra]
sqrtr_pnat_div_neq0 [in QBS.normal_algebra]
standard_borel_lr_sets_ident [in QBS.measure_qbs_adjunction]
sub_qbs_Mx_glue [in QBS.quasi_borel]
sub_qbs_Mx_const [in QBS.quasi_borel]
sub_qbs_Mx_comp [in QBS.quasi_borel]
U
unit_to_pair_snd_le1 [in QBS.standard_borel]unit_to_pair_snd_ge0 [in QBS.standard_borel]
unit_to_pair_fst_le1 [in QBS.standard_borel]
unit_to_pair_fst_ge0 [in QBS.standard_borel]
unit_to_pairK [in QBS.standard_borel]
V
variance_prod_snd [in QBS.pair_qbs_measure]variance_prod_fst [in QBS.pair_qbs_measure]
var_recurrence [in QBS.normal_algebra]
Constructor Index
G
gen_glue [in QBS.quasi_borel]gen_const [in QBS.quasi_borel]
gen_comp [in QBS.quasi_borel]
gen_base [in QBS.quasi_borel]
Projection Index
I
isQBSMorphism.qbs_hom_proof [in QBS.quasi_borel]isQBS.qbs_Mx_glue [in QBS.quasi_borel]
isQBS.qbs_Mx_const [in QBS.quasi_borel]
isQBS.qbs_Mx_comp [in QBS.quasi_borel]
isQBS.qbs_Mx [in QBS.quasi_borel]
Q
QBSHom.class [in QBS.quasi_borel]QBSHom.quasi_borel_isQBSMorphism_mixin [in QBS.quasi_borel]
QBSHom.sort [in QBS.quasi_borel]
QBSpace.class [in QBS.quasi_borel]
QBSpace.quasi_borel_isQBS_mixin [in QBS.quasi_borel]
QBSpace.sort [in QBS.quasi_borel]
qbs_prob_alpha_random [in QBS.probability_qbs]
qbs_prob_mu [in QBS.probability_qbs]
qbs_prob_alpha [in QBS.probability_qbs]
qps_repr [in QBS.qbs_prob_quot]
S
sb_retractK [in QBS.measure_qbs_adjunction]sb_decode [in QBS.measure_qbs_adjunction]
sb_encode [in QBS.measure_qbs_adjunction]
Inductive Index
G
generating_Mx [in QBS.quasi_borel]Section Index
B
bayesian_regression [in QBS.showcase.bayesian_regression]binary_digit_interleaving.composed_bijection [in QBS.standard_borel]
binary_digit_interleaving.measurability_constructions [in QBS.standard_borel]
binary_digit_interleaving.round_trips [in QBS.standard_borel]
binary_digit_interleaving.pairing_reconstruction [in QBS.standard_borel]
binary_digit_interleaving.binary_digit_arithmetic [in QBS.standard_borel]
binary_digit_interleaving [in QBS.standard_borel]
C
coproduct_qbs.listQ_instance [in QBS.coproduct_qbs]coproduct_qbs.piQ_instance [in QBS.coproduct_qbs]
coproduct_qbs.gen_coprodQ_instance [in QBS.coproduct_qbs]
coproduct_qbs.coprodQ_instance [in QBS.coproduct_qbs]
coproduct_qbs [in QBS.coproduct_qbs]
I
integral_normal_prob [in QBS.showcase.bayesian_regression]isQBSMorphism.isQBSMorphism.isQBSMorphism [in QBS.quasi_borel]
isQBS.isQBS.isQBS [in QBS.quasi_borel]
M
measure_as_qbs.distribution_expectations [in QBS.measure_as_qbs_measure]measure_as_qbs [in QBS.measure_as_qbs_measure]
mqa [in QBS.measure_qbs_adjunction]
N
normal_density_algebra.bayesian_phase2_slope [in QBS.normal_algebra]normal_density_algebra.bayesian_phase1_intercept [in QBS.normal_algebra]
normal_density_algebra.normal_pdf_general [in QBS.normal_algebra]
normal_density_algebra [in QBS.normal_algebra]
P
pair_qbs_measure.pair_mu_build [in QBS.pair_qbs_measure]pair_qbs_measure [in QBS.pair_qbs_measure]
phi_psi [in QBS.standard_borel]
probability_qbs.qbs_normalize_def [in QBS.probability_qbs]
probability_qbs.normalize_mu_build [in QBS.probability_qbs]
probability_qbs.probability_inequalities [in QBS.probability_qbs]
probability_qbs.strength_and_monad_structure [in QBS.probability_qbs]
probability_qbs.bind_congruence [in QBS.probability_qbs]
probability_qbs.monad_operations [in QBS.probability_qbs]
probability_qbs.qbs_integration [in QBS.probability_qbs]
probability_qbs.monad_bind [in QBS.probability_qbs]
probability_qbs.probability_monad.monadP_instance [in QBS.probability_qbs]
probability_qbs.probability_monad [in QBS.probability_qbs]
probability_qbs.qbs_prob_basics [in QBS.probability_qbs]
probability_qbs [in QBS.probability_qbs]
Q
qbs [in QBS.quasi_borel]qbs_kernel.round_trip [in QBS.qbs_kernel]
qbs_kernel.integration [in QBS.qbs_kernel]
qbs_kernel.bind_return [in QBS.qbs_kernel]
qbs_kernel.dirac_comp [in QBS.qbs_kernel]
qbs_kernel.giry_pushforward [in QBS.qbs_kernel]
qbs_kernel.equiv_kernel [in QBS.qbs_kernel]
qbs_kernel.const_kernel [in QBS.qbs_kernel]
qbs_kernel.kdirac_measurability [in QBS.qbs_kernel]
qbs_kernel.qbs_morph_kernel [in QBS.qbs_kernel]
qbs_kernel.qbs_return_dirac [in QBS.qbs_kernel]
qbs_kernel.kdirac_unfold [in QBS.qbs_kernel]
qbs_kernel.pushforward_prob [in QBS.qbs_kernel]
qbs_kernel [in QBS.qbs_kernel]
qbs_prob_quot.qbs_prob_space_instance [in QBS.qbs_prob_quot]
qbs_prob_quot [in QBS.qbs_prob_quot]
qbs_giry.giry_to_qbs [in QBS.qbs_giry]
qbs_giry.qbs_to_giry [in QBS.qbs_giry]
qbs_giry [in QBS.qbs_giry]
qbs_quotient.monad_laws_quot [in QBS.qbs_quotient]
qbs_quotient.well_defined [in QBS.qbs_quotient]
qbs_quotient.lifted_ops [in QBS.qbs_quotient]
qbs_quotient.quotient_def [in QBS.qbs_quotient]
qbs_quotient.equiv_instances [in QBS.qbs_quotient]
qbs_quotient [in QBS.qbs_quotient]
qbs.expQ_instance [in QBS.quasi_borel]
qbs.generating_qbs_instance [in QBS.quasi_borel]
qbs.prodQ_instance [in QBS.quasi_borel]
qbs.qbs_order [in QBS.quasi_borel]
qbs.qbs_unit_instance [in QBS.quasi_borel]
qbs.qbs_curry_instance [in QBS.quasi_borel]
qbs.qbs_eval_instance [in QBS.quasi_borel]
qbs.qbs_pair_instance [in QBS.quasi_borel]
qbs.qbs_snd_instance [in QBS.quasi_borel]
qbs.qbs_fst_instance [in QBS.quasi_borel]
qbs.qbs_const_instance [in QBS.quasi_borel]
qbs.qbs_comp_instance [in QBS.quasi_borel]
qbs.qbs_id_instance [in QBS.quasi_borel]
qbs.R_qbs_instance [in QBS.quasi_borel]
qbs.sub_qbs_def [in QBS.quasi_borel]
qbs.unitQ_instance [in QBS.quasi_borel]
S
standard_borel_mR [in QBS.standard_borel]Abbreviation Index
I
isQBS [in QBS.quasi_borel]isQBSMorphism [in QBS.quasi_borel]
isQBSMorphism.axioms [in QBS.quasi_borel]
isQBSMorphism.Build [in QBS.quasi_borel]
isQBS.axioms [in QBS.quasi_borel]
isQBS.Build [in QBS.quasi_borel]
L
L_sigma [in QBS.measure_qbs_adjunction]M
mR [in QBS.coproduct_qbs]mR [in QBS.qbs_kernel]
mR [in QBS.probability_qbs]
mR [in QBS.measure_qbs_adjunction]
mR [in QBS.qbs_prob_quot]
mR [in QBS.qbs_giry]
mR [in QBS.showcase.bayesian_regression]
mR [in QBS.pair_qbs_measure]
mR [in QBS.qbs_quotient]
mR [in QBS.measure_as_qbs_measure]
mR [in QBS.quasi_borel]
mR [in QBS.standard_borel]
mu [in QBS.showcase.bayesian_regression]
P
piX [in QBS.qbs_quotient]piX [in QBS.qbs_quotient]
piX [in QBS.qbs_quotient]
piY [in QBS.qbs_quotient]
piY [in QBS.qbs_quotient]
piY [in QBS.qbs_quotient]
Q
QBSHom [in QBS.quasi_borel]QBSHom.clone [in QBS.quasi_borel]
QBSHom.copy [in QBS.quasi_borel]
QBSHom.Exports.qbsHomType [in QBS.quasi_borel]
QBSHom.on [in QBS.quasi_borel]
QBSHom.on_ [in QBS.quasi_borel]
QBSpace [in QBS.quasi_borel]
QBSpace.clone [in QBS.quasi_borel]
QBSpace.copy [in QBS.quasi_borel]
QBSpace.Exports.qbsType [in QBS.quasi_borel]
QBSpace.on [in QBS.quasi_borel]
QBSpace.on_ [in QBS.quasi_borel]
T
truncnP [in QBS.measure_qbs_adjunction]Definition Index
A
as_qbs_prob [in QBS.measure_as_qbs_measure]B
bin_digits [in QBS.standard_borel]bin_sum [in QBS.standard_borel]
bin_partial_sum [in QBS.standard_borel]
bin_digit [in QBS.standard_borel]
boolQ [in QBS.quasi_borel]
C
choice_Choice__to__eqtype_hasDecEq [in QBS.qbs_quotient]choice_Choice__to__choice_hasChoice [in QBS.qbs_quotient]
const_kernel_of_qbs [in QBS.qbs_kernel]
coprodQ [in QBS.coproduct_qbs]
coprodQ_random [in QBS.coproduct_qbs]
D
d [in QBS.showcase.bayesian_regression]Datatypes_list__canonical__quasi_borel_QBSpace [in QBS.coproduct_qbs]
Datatypes_sum__canonical__quasi_borel_QBSpace [in QBS.coproduct_qbs]
Datatypes_unit__canonical__quasi_borel_QBSpace [in QBS.quasi_borel]
Datatypes_prod__canonical__quasi_borel_QBSpace [in QBS.quasi_borel]
decode_RR_mR [in QBS.standard_borel]
decode_RR [in QBS.standard_borel]
deinterleave_odd [in QBS.standard_borel]
deinterleave_even [in QBS.standard_borel]
E
encode_RR_mR [in QBS.standard_borel]encode_RR [in QBS.standard_borel]
erealQ [in QBS.measure_qbs_adjunction]
evidence [in QBS.showcase.bayesian_regression]
expQ [in QBS.quasi_borel]
G
gaussian_prod_scalar [in QBS.normal_algebra]gaussian_prod_sigma [in QBS.normal_algebra]
gaussian_prod_mu [in QBS.normal_algebra]
generating_qbs [in QBS.quasi_borel]
generating_Mx_sind [in QBS.quasi_borel]
generating_Mx_ind [in QBS.quasi_borel]
generic_quotient_EqQuotient__to__generic_quotient_isEqQuotient [in QBS.qbs_quotient]
generic_quotient_EqQuotient__to__generic_quotient_isQuotient [in QBS.qbs_quotient]
gen_coprodQ [in QBS.coproduct_qbs]
gen_coprodQ_random [in QBS.coproduct_qbs]
giry_to_qbs [in QBS.qbs_giry]
H
HB_unnamed_factory_7 [in QBS.coproduct_qbs]HB_unnamed_factory_5 [in QBS.coproduct_qbs]
HB_unnamed_factory_3 [in QBS.coproduct_qbs]
HB_unnamed_factory_1 [in QBS.coproduct_qbs]
HB_unnamed_mixin_18 [in QBS.probability_qbs]
HB_unnamed_mixin_17 [in QBS.probability_qbs]
HB_unnamed_mixin_16 [in QBS.probability_qbs]
HB_unnamed_mixin_15 [in QBS.probability_qbs]
HB_unnamed_mixin_14 [in QBS.probability_qbs]
HB_unnamed_factory_8 [in QBS.probability_qbs]
HB_unnamed_mixin_7 [in QBS.probability_qbs]
HB_unnamed_mixin_6 [in QBS.probability_qbs]
HB_unnamed_factory_3 [in QBS.probability_qbs]
HB_unnamed_factory_1 [in QBS.probability_qbs]
HB_unnamed_factory_1 [in QBS.qbs_prob_quot]
HB_unnamed_mixin_39 [in QBS.qbs_giry]
HB_unnamed_mixin_38 [in QBS.qbs_giry]
HB_unnamed_mixin_37 [in QBS.qbs_giry]
HB_unnamed_mixin_36 [in QBS.qbs_giry]
HB_unnamed_mixin_35 [in QBS.qbs_giry]
HB_unnamed_factory_24 [in QBS.qbs_giry]
HB_unnamed_mixin_23 [in QBS.qbs_giry]
HB_unnamed_mixin_22 [in QBS.qbs_giry]
HB_unnamed_factory_17 [in QBS.qbs_giry]
HB_unnamed_mixin_16 [in QBS.qbs_giry]
HB_unnamed_mixin_15 [in QBS.qbs_giry]
HB_unnamed_mixin_14 [in QBS.qbs_giry]
HB_unnamed_mixin_13 [in QBS.qbs_giry]
HB_unnamed_mixin_12 [in QBS.qbs_giry]
HB_unnamed_factory_6 [in QBS.qbs_giry]
HB_unnamed_mixin_5 [in QBS.qbs_giry]
HB_unnamed_mixin_4 [in QBS.qbs_giry]
HB_unnamed_factory_1 [in QBS.qbs_giry]
HB_unnamed_mixin_16 [in QBS.pair_qbs_measure]
HB_unnamed_mixin_15 [in QBS.pair_qbs_measure]
HB_unnamed_mixin_14 [in QBS.pair_qbs_measure]
HB_unnamed_mixin_13 [in QBS.pair_qbs_measure]
HB_unnamed_mixin_12 [in QBS.pair_qbs_measure]
HB_unnamed_factory_6 [in QBS.pair_qbs_measure]
HB_unnamed_mixin_5 [in QBS.pair_qbs_measure]
HB_unnamed_mixin_4 [in QBS.pair_qbs_measure]
HB_unnamed_factory_1 [in QBS.pair_qbs_measure]
HB_unnamed_mixin_15 [in QBS.qbs_quotient]
HB_unnamed_mixin_14 [in QBS.qbs_quotient]
HB_unnamed_factory_10 [in QBS.qbs_quotient]
HB_unnamed_mixin_9 [in QBS.qbs_quotient]
HB_unnamed_mixin_8 [in QBS.qbs_quotient]
HB_unnamed_factory_5 [in QBS.qbs_quotient]
HB_unnamed_factory_3 [in QBS.qbs_quotient]
HB_unnamed_factory_1 [in QBS.qbs_quotient]
HB_unnamed_factory_34 [in QBS.quasi_borel]
HB_unnamed_factory_32 [in QBS.quasi_borel]
HB_unnamed_factory_29 [in QBS.quasi_borel]
HB_unnamed_factory_27 [in QBS.quasi_borel]
HB_unnamed_factory_25 [in QBS.quasi_borel]
HB_unnamed_factory_22 [in QBS.quasi_borel]
HB_unnamed_factory_20 [in QBS.quasi_borel]
HB_unnamed_factory_18 [in QBS.quasi_borel]
HB_unnamed_factory_15 [in QBS.quasi_borel]
HB_unnamed_factory_12 [in QBS.quasi_borel]
HB_unnamed_factory_10 [in QBS.quasi_borel]
HB_unnamed_factory_8 [in QBS.quasi_borel]
HB_unnamed_factory_5 [in QBS.quasi_borel]
HB_unnamed_factory_3 [in QBS.quasi_borel]
HB_unnamed_factory_1 [in QBS.quasi_borel]
I
intercept_prior [in QBS.showcase.bayesian_regression]interleave [in QBS.standard_borel]
isQBSMorphism.identity_builder [in QBS.quasi_borel]
isQBSMorphism.phant_axioms [in QBS.quasi_borel]
isQBSMorphism.phant_Build [in QBS.quasi_borel]
isQBS.identity_builder [in QBS.quasi_borel]
isQBS.phant_axioms [in QBS.quasi_borel]
isQBS.phant_Build [in QBS.quasi_borel]
L
likelihood_single [in QBS.showcase.bayesian_regression]listQ [in QBS.coproduct_qbs]
listQ_random [in QBS.coproduct_qbs]
M
map_qbs [in QBS.quasi_borel]measfun_kernel [in QBS.qbs_kernel]
Measurable_sort__canonical__quasi_borel_QBSpace [in QBS.quasi_borel]
measure_function_isMeasure__to__measure_function_isContent [in QBS.probability_qbs]
measure_function_isMeasure__to__measure_function_Content_isMeasure [in QBS.probability_qbs]
measure_function_isMeasure__to__measure_function_isContent__21 [in QBS.qbs_giry]
measure_function_isMeasure__to__measure_function_Content_isMeasure__19 [in QBS.qbs_giry]
measure_function_isMeasure__to__measure_function_isContent [in QBS.qbs_giry]
measure_function_isMeasure__to__measure_function_Content_isMeasure [in QBS.qbs_giry]
measure_function_isMeasure__to__measure_function_isContent [in QBS.pair_qbs_measure]
measure_function_isMeasure__to__measure_function_Content_isMeasure [in QBS.pair_qbs_measure]
monadP [in QBS.probability_qbs]
monadP_map [in QBS.probability_qbs]
monadP_random_pw [in QBS.probability_qbs]
monadP_random [in QBS.probability_qbs]
N
natQ [in QBS.quasi_borel]normalize_prob [in QBS.probability_qbs]
normalize_mu [in QBS.probability_qbs]
norm_qbs [in QBS.showcase.bayesian_regression]
no_trailing_ones [in QBS.standard_borel]
O
obs [in QBS.showcase.bayesian_regression]P
pair_qbs_measure_pf_mu__canonical__probability_measure_Probability [in QBS.pair_qbs_measure]pair_qbs_measure_pf_mu__canonical__probability_measure_SubProbability [in QBS.pair_qbs_measure]
pair_qbs_measure_pf_mu__canonical__measure_function_FiniteMeasure [in QBS.pair_qbs_measure]
pair_qbs_measure_pf_mu__canonical__measure_function_FinNumFun [in QBS.pair_qbs_measure]
pair_qbs_measure_pf_mu__canonical__measure_function_SigmaFiniteMeasure [in QBS.pair_qbs_measure]
pair_qbs_measure_pf_mu__canonical__measure_function_SFiniteMeasure [in QBS.pair_qbs_measure]
pair_qbs_measure_pf_mu__canonical__measure_function_SigmaFiniteContent [in QBS.pair_qbs_measure]
pair_qbs_measure_pf_mu__canonical__measure_function_Measure [in QBS.pair_qbs_measure]
pair_qbs_measure_pf_mu__canonical__measure_function_Content [in QBS.pair_qbs_measure]
pair_to_unit [in QBS.standard_borel]
phase2_const [in QBS.normal_algebra]
phase2_final_sigma [in QBS.normal_algebra]
phase2_final_mu [in QBS.normal_algebra]
phi [in QBS.standard_borel]
piQ [in QBS.coproduct_qbs]
piQ_random [in QBS.coproduct_qbs]
posterior_density [in QBS.showcase.bayesian_regression]
predictive_integral [in QBS.showcase.bayesian_regression]
prior [in QBS.showcase.bayesian_regression]
prior_bind [in QBS.showcase.bayesian_regression]
prior_inner [in QBS.showcase.bayesian_regression]
probability_qbs_norm_mu__canonical__probability_measure_Probability [in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__probability_measure_SubProbability [in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__measure_function_FiniteMeasure [in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__measure_function_FinNumFun [in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__measure_function_SigmaFiniteMeasure [in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__measure_function_SFiniteMeasure [in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__measure_function_SigmaFiniteContent [in QBS.probability_qbs]
probability_measure_Measure_isProbability__to__measure_function_isFinite [in QBS.probability_qbs]
probability_measure_Measure_isProbability__to__measure_function_isSFinite [in QBS.probability_qbs]
probability_measure_Measure_isProbability__to__probability_measure_isSubProbability [in QBS.probability_qbs]
probability_measure_Measure_isProbability__to__measure_function_isSigmaFinite [in QBS.probability_qbs]
probability_measure_Measure_isProbability__to__probability_measure_isProbability [in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__measure_function_Measure [in QBS.probability_qbs]
probability_qbs_norm_mu__canonical__measure_function_Content [in QBS.probability_qbs]
probability_qbs_qbs_prob__canonical__quasi_borel_QBSpace [in QBS.probability_qbs]
probability_measure_Measure_isProbability__to__measure_function_isFinite__34 [in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__measure_function_isSFinite__32 [in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__probability_measure_isSubProbability__30 [in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__measure_function_isSigmaFinite__28 [in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__probability_measure_isProbability__26 [in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__measure_function_isFinite [in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__measure_function_isSFinite [in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__probability_measure_isSubProbability [in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__measure_function_isSigmaFinite [in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__probability_measure_isProbability [in QBS.qbs_giry]
probability_measure_Measure_isProbability__to__measure_function_isFinite [in QBS.pair_qbs_measure]
probability_measure_Measure_isProbability__to__measure_function_isSFinite [in QBS.pair_qbs_measure]
probability_measure_Measure_isProbability__to__probability_measure_isSubProbability [in QBS.pair_qbs_measure]
probability_measure_Measure_isProbability__to__measure_function_isSigmaFinite [in QBS.pair_qbs_measure]
probability_measure_Measure_isProbability__to__probability_measure_isProbability [in QBS.pair_qbs_measure]
probability_qbs_qbs_prob__canonical__choice_Choice [in QBS.qbs_quotient]
probability_qbs_qbs_prob__canonical__eqtype_Equality [in QBS.qbs_quotient]
prodQ [in QBS.quasi_borel]
prod__canonical__quasi_borel_QBSpace [in QBS.coproduct_qbs]
program [in QBS.showcase.bayesian_regression]
psi [in QBS.standard_borel]
Q
QBSHom_type__canonical__quasi_borel_QBSpace [in QBS.quasi_borel]QBSHom.pack_ [in QBS.quasi_borel]
QBSHom.phant_on_ [in QBS.quasi_borel]
QBSHom.phant_clone [in QBS.quasi_borel]
QBSpace.pack_ [in QBS.quasi_borel]
QBSpace.phant_on_ [in QBS.quasi_borel]
QBSpace.phant_clone [in QBS.quasi_borel]
qbs_morph_kdirac [in QBS.qbs_kernel]
qbs_normalize [in QBS.probability_qbs]
qbs_rv [in QBS.probability_qbs]
qbs_integrable [in QBS.probability_qbs]
qbs_strength [in QBS.probability_qbs]
qbs_join [in QBS.probability_qbs]
qbs_variance [in QBS.probability_qbs]
qbs_prob_event [in QBS.probability_qbs]
qbs_expect [in QBS.probability_qbs]
qbs_measurable [in QBS.probability_qbs]
qbs_integral [in QBS.probability_qbs]
qbs_bind_strong [in QBS.probability_qbs]
qbs_bind [in QBS.probability_qbs]
qbs_morphism_strong [in QBS.probability_qbs]
qbs_return [in QBS.probability_qbs]
qbs_prob_equiv [in QBS.probability_qbs]
qbs_prob_space_qbs [in QBS.qbs_prob_quot]
qbs_prob_quot_qbs_prob_space__canonical__quasi_borel_QBSpace [in QBS.qbs_prob_quot]
qbs_giry_pf_mu__canonical__probability_measure_Probability [in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__probability_measure_SubProbability [in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__measure_function_FiniteMeasure [in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__measure_function_FinNumFun [in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__measure_function_SigmaFiniteMeasure [in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__measure_function_SFiniteMeasure [in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__measure_function_SigmaFiniteContent [in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__measure_function_Measure [in QBS.qbs_giry]
qbs_giry_pf_mu__canonical__measure_function_Content [in QBS.qbs_giry]
qbs_to_giry [in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__probability_measure_Probability [in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__probability_measure_SubProbability [in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__measure_function_FiniteMeasure [in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__measure_function_FinNumFun [in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__measure_function_SigmaFiniteMeasure [in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__measure_function_SFiniteMeasure [in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__measure_function_SigmaFiniteContent [in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__measure_function_Measure [in QBS.qbs_giry]
qbs_giry_qbs_to_giry_mu__canonical__measure_function_Content [in QBS.qbs_giry]
qbs_to_giry_mu [in QBS.qbs_giry]
qbs_pair_variance [in QBS.pair_qbs_measure]
qbs_indep [in QBS.pair_qbs_measure]
qbs_pair_fun [in QBS.pair_qbs_measure]
qbs_pair_integral [in QBS.pair_qbs_measure]
qbs_prob_pair [in QBS.pair_qbs_measure]
qbs_pair_mu [in QBS.pair_qbs_measure]
qbs_pair_alpha [in QBS.pair_qbs_measure]
qbs_pair_mu_build [in QBS.pair_qbs_measure]
qbs_quotient_qbs_quot__canonical__generic_quotient_EqQuotient [in QBS.qbs_quotient]
qbs_quotient_qbs_quot__canonical__generic_quotient_Quotient [in QBS.qbs_quotient]
qbs_quotient_qbs_quot__canonical__choice_Choice [in QBS.qbs_quotient]
qbs_quotient_qbs_quot__canonical__eqtype_Equality [in QBS.qbs_quotient]
qbs_quot [in QBS.qbs_quotient]
qbs_prob_equivRel [in QBS.qbs_quotient]
qbs_equiv_op [in QBS.qbs_quotient]
qbs_uniform [in QBS.measure_as_qbs_measure]
qbs_bernoulli [in QBS.measure_as_qbs_measure]
qbs_normal_distribution [in QBS.measure_as_qbs_measure]
qbs_supT [in QBS.quasi_borel]
qbs_leT [in QBS.quasi_borel]
qbs_mul [in QBS.quasi_borel]
qbs_add [in QBS.quasi_borel]
qbs_unit [in QBS.quasi_borel]
qbs_curry [in QBS.quasi_borel]
qbs_eval [in QBS.quasi_borel]
qbs_pair [in QBS.quasi_borel]
qbs_snd [in QBS.quasi_borel]
qbs_fst [in QBS.quasi_borel]
qbs_const [in QBS.quasi_borel]
qbs_comp [in QBS.quasi_borel]
qbs_id [in QBS.quasi_borel]
qbs_morphism [in QBS.quasi_borel]
qbs_hom_proof [in QBS.quasi_borel]
qbs_Mx_glue [in QBS.quasi_borel]
qbs_Mx_const [in QBS.quasi_borel]
qbs_Mx_comp [in QBS.quasi_borel]
qbs_Mx [in QBS.quasi_borel]
qps_pick_repr [in QBS.qbs_prob_quot]
qps_prob_event [in QBS.qbs_prob_quot]
qps_expect [in QBS.qbs_prob_quot]
qps_map [in QBS.qbs_prob_quot]
qps_integral [in QBS.qbs_prob_quot]
qps_bind_strong [in QBS.qbs_prob_quot]
qps_bind [in QBS.qbs_prob_quot]
qps_return [in QBS.qbs_prob_quot]
qps_of [in QBS.qbs_prob_quot]
qps_eq [in QBS.qbs_prob_quot]
quasi_borel_T__canonical__quasi_borel_QBSpace [in QBS.quasi_borel]
quasi_borel_sub_car__canonical__quasi_borel_QBSpace [in QBS.quasi_borel]
quasi_borel_f__canonical__quasi_borel_QBSHom__31 [in QBS.quasi_borel]
quasi_borel_curry_fun__canonical__quasi_borel_QBSHom [in QBS.quasi_borel]
quasi_borel_f__canonical__quasi_borel_QBSHom__24 [in QBS.quasi_borel]
quasi_borel_fg__canonical__quasi_borel_QBSHom [in QBS.quasi_borel]
quasi_borel_f__canonical__quasi_borel_QBSHom__17 [in QBS.quasi_borel]
quasi_borel_f__canonical__quasi_borel_QBSHom__14 [in QBS.quasi_borel]
quasi_borel_f__canonical__quasi_borel_QBSHom__7 [in QBS.quasi_borel]
quasi_borel_gf__canonical__quasi_borel_QBSHom [in QBS.quasi_borel]
quasi_borel_f__canonical__quasi_borel_QBSHom [in QBS.quasi_borel]
quot_bind_strong [in QBS.qbs_quotient]
quot_map [in QBS.qbs_quotient]
quot_integral [in QBS.qbs_quotient]
quot_return [in QBS.qbs_quotient]
R
realQ [in QBS.quasi_borel]R_qbs [in QBS.quasi_borel]
S
scalar_of_s [in QBS.showcase.bayesian_regression]sigma_Mx [in QBS.quasi_borel]
slope_prior [in QBS.showcase.bayesian_regression]
Specif_sigT__canonical__quasi_borel_QBSpace [in QBS.coproduct_qbs]
sub_qbs [in QBS.quasi_borel]
U
unitQ [in QBS.quasi_borel]unit_to_pair [in QBS.standard_borel]
Record Index
I
isQBSMorphism.axioms_ [in QBS.quasi_borel]isQBS.axioms_ [in QBS.quasi_borel]
Q
QBSHom.axioms_ [in QBS.quasi_borel]QBSHom.type [in QBS.quasi_borel]
QBSpace.axioms_ [in QBS.quasi_borel]
QBSpace.type [in QBS.quasi_borel]
qbs_prob [in QBS.probability_qbs]
qbs_prob_space [in QBS.qbs_prob_quot]
S
standard_borel_wit [in QBS.measure_qbs_adjunction]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1105 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (251 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (375 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (18 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (79 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (39 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (306 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |
This page has been generated by coqdoc